We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent a5bee96 commit 039121bCopy full SHA for 039121b
tests/regression/01-cpa/30-extern_var.c
@@ -1,9 +1,15 @@
1
#include <goblint.h>
2
3
-extern int q;
+int p; // assumed to be 0-initialized
4
+extern int q; // not assumed to be 0-initialized
5
-int main(){
6
- int i = q ? 1 : 2 ;
7
- __goblint_check(0); // FAIL
+int main() {
+ __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!
14
return 0;
15
}
0 commit comments