Skip to content

Commit 0492c36

Browse files
committed
Test comparison operator result integer bounds
1 parent a06dc86 commit 0492c36

2 files changed

Lines changed: 11 additions & 1 deletion

File tree

tests/regression/01-cpa/28-interval.c

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,11 @@ int main () {
4949
__goblint_check(!(a>9));
5050
__goblint_check(b==8); //UNKNOWN
5151

52+
__goblint_check((a < 10) == 1);
53+
__goblint_check((a > 9) == 0);
54+
__goblint_check((a == b) >= 0);
55+
__goblint_check((a == b) <= 1);
56+
5257
for(x = 0; x < 10; x++){
5358
__goblint_check(x >= 0);
5459
__goblint_check(x <= 9);

tests/regression/57-floats/01-base.c

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// PARAM: --enable ana.float.interval
1+
// PARAM: --enable ana.float.interval --enable ana.int.interval
22
#include <goblint.h>
33
#include <float.h>
44
#include <limits.h>
@@ -23,6 +23,11 @@ int main()
2323
__goblint_check(a < 10.); // SUCCESS
2424
__goblint_check(a > 10.); // FAIL
2525

26+
__goblint_check((a < 10.) == 1);
27+
__goblint_check((a > 10.) == 0);
28+
__goblint_check((x == 2.) >= 0); // TODO
29+
__goblint_check((x == 2.) <= 1); // TODO
30+
2631
__goblint_check(c == 2.f); // SUCCESS
2732
__goblint_check(c < 10.f); // SUCCESS
2833
__goblint_check(c > 10.f); // FAIL

0 commit comments

Comments
 (0)