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

edwin@fedora38 ~/…/lint/lintcstubs [4.14.1] ❯ 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);
}

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:24:3-24:31)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (x.c:24:3-24: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)
Pruning result
[Info][Deadcode] Logical lines of code (LLoC) summary:
live: 9
dead: 0
total: 9
edwin@fedora38 ~/…/lint/lintcstubs [4.14.1] ❯ goblint --version
Goblint version: 2.1.0-1-g80bd97e (heads/master-0-g80bd97e6b-dirty)
Cil version: 2.0.1
Profile: release

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