Skip to content

Commit 3f300b1

Browse files
authored
Merge pull request #1842 from goblint/cpa-extern_var-test
Fix test 01-cpa/30-extern_var
2 parents d5d0805 + 039121b commit 3f300b1

File tree

1 file changed

+10
-4
lines changed

1 file changed

+10
-4
lines changed
Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,15 @@
11
#include <goblint.h>
22

3-
extern int q;
3+
int p; // assumed to be 0-initialized
4+
extern int q; // not assumed to be 0-initialized
45

5-
int main(){
6-
int i = q ? 1 : 2 ;
7-
__goblint_check(0); // FAIL
6+
int main() {
7+
__goblint_check(p == 0);
8+
__goblint_check(q == 0); // UNKNOWN!
9+
10+
p = 42;
11+
q = 42; // does not stick because extern may be modified externally
12+
__goblint_check(p == 42);
13+
__goblint_check(q == 42); // UNKNOWN!
814
return 0;
915
}

0 commit comments

Comments
 (0)