Skip to content

Commit a95089a

Browse files
Add tests for annotations also for context
1 parent acd7cfd commit a95089a

File tree

2 files changed

+30
-0
lines changed

2 files changed

+30
-0
lines changed
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// PARAM: --enable ana.int.interval --disable ana.context.widen --enable ana.base.context.int --set annotation.goblint_context.base.no-int[+] f
2+
#include <assert.h>
3+
4+
int f(int x) {
5+
if (x)
6+
return f(x+1);
7+
else
8+
return x;
9+
}
10+
11+
int main () {
12+
int a = f(1);
13+
assert(!a);
14+
return 0;
15+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// PARAM: --enable ana.int.interval --disable ana.context.widen --disable ana.base.context.int --set annotation.goblint_context.base.int[+] f
2+
#include <assert.h>
3+
4+
int f(int x) {
5+
if (x)
6+
return x * f(x - 1);
7+
else
8+
return 1;
9+
}
10+
11+
int main () {
12+
int a = f(10);
13+
assert(a == 3628800);
14+
return 0;
15+
}

0 commit comments

Comments
 (0)