Skip to content

Instantly share code, notes, and snippets.

@edwintorok

edwintorok/gist:8c6f3de4f717a3145945705cdcbe863b Secret

Created September 9, 2023 17:50
Show Gist options
  • Save edwintorok/8c6f3de4f717a3145945705cdcbe863b to your computer and use it in GitHub Desktop.
Save edwintorok/8c6f3de4f717a3145945705cdcbe863b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
cat x.c
#include <goblint.h>
#include <assert.h>
int __VERIFIER_nondet_int(void);
int foo(long x)
{
__goblint_assume(x&1);
assert(x&1);
}
int main()
{
foo(__VERIFIER_nondet_int());
}
edwin@fedora38 ~/…/lint/lintcstubs [4.14.1] ❯ goblint x.c --enable ana.int.congruence --conf examples/very-precise.json --set 'ana.activated[+]' assert --set 'sem.int.signed_overflow' 'assume_none'
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (x.c:12:3-12:31)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (x.c:6:3-6:24)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (x.c:7:3-7:24)
[Warning][Assert] Assertion "(int )(x & 1L)" is unknown. (x.c:7:3-7:24)
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 7
dead: 0
total: 7
@edwintorok
Copy link
Author

cat x.c
#include <goblint.h>
#include <assert.h>

#define __VERIFIER_nondet2(X, Y)
X _VERIFIER_nondet##Y() attribute((goblint_stub));
X _VERIFIER_nondet##Y() { X val; return val; }
#define __VERIFIER_nondet(X) __VERIFIER_nondet2(X, X)

typedef unsigned int uint;
__VERIFIER_nondet(uint);

unsigned int __VERIFIER_nondet_uint(void);
int foo(unsigned long x)
{
__goblint_assume(!!(x&1));
assert(!!(x&1));
__goblint_assume(x&1);
assert(x&1);

__goblint_assume(x%2);
assert(x%2);
}

int main()
{
foo(__VERIFIER_nondet_int());
}
edwin@fedora38 ~/…/lint/lintcstubs [4.14.1] ❯ goblint x.c --conf examples/very-precise.json --set 'ana.activated[+]' assert --set 'sem.int.signed_overflow' 'assume_none' --enable ana.int.congruence --enable dbg.debug
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (x.c:27:3-27:31)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (x.c:27:3-27:31)
[Warning][Assert] Assertion "! (! (x & 1UL))" is unknown. (x.c:17:3-17:28)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (x.c:18:3-18:24)
[Debug][Analyzer] Invariant failed: expression "CastE(TInt(int, ), &(Lval(Var(x, NoOffset)), Const(Int(1,unsigned long,None))))" not understood. (x.c:18:3-18:24)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (x.c:19:3-19:24)
[Debug][Analyzer] Invariant failed: expression "CastE(TInt(int, ), &(Lval(Var(x, NoOffset)), Const(Int(1,unsigned long,None))))" not understood. (x.c:19:3-19:24)
[Warning][Assert] Assertion "(int )(x & 1UL)" is unknown. (x.c:19:3-19:24)
[Debug][Analyzer] Invariant failed: expression "CastE(TInt(int, ), %(Lval(Var(x, NoOffset)), Const(Int(2,unsigned long,None))))" not understood. (x.c:21:3-21:24)
[Debug][Analyzer] Invariant failed: expression "CastE(TInt(int, ), %(Lval(Var(x, NoOffset)), Const(Int(2,unsigned long,None))))" not understood. (x.c:22:3-22:24)
[Warning][Assert] Assertion "(int )(x % 2UL)" is unknown. (x.c:22:3-22:24)
Pruning result
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 11
dead: 0
total: 11

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment