Skip to content

Commit b46dc0f

Browse files
committed
Fix test 82/04 widening gas
The old test had no widening at all, since there was only one side effect per variable. Also changed so that one variable has more side effects than gas.
1 parent 64411f6 commit b46dc0f

File tree

1 file changed

+10
-3
lines changed

1 file changed

+10
-3
lines changed

tests/regression/82-widening_gas/04-side_simple_update.c

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 3 --enable ana.int.interval --enable exp.earlyglobs
1+
// PARAM: --set solvers.td3.side_widen always --set solvers.td3.side_widen_gas 2 --enable ana.int.interval --enable exp.earlyglobs
22
#include <pthread.h>
33
#include <goblint.h>
44

@@ -12,11 +12,18 @@ void *thread(void *arg) {
1212
pthread_mutex_lock(&A);
1313
a = 1;
1414
b = 1;
15-
b = 2;
1615
c = 1;
16+
pthread_mutex_unlock(&A);
17+
18+
pthread_mutex_lock(&A);
19+
b = 2;
1720
c = 2;
1821
c = 3;
1922
pthread_mutex_unlock(&A);
23+
24+
pthread_mutex_lock(&A);
25+
c = 4;
26+
pthread_mutex_unlock(&A);
2027
return NULL;
2128
}
2229

@@ -28,7 +35,7 @@ int main(void) {
2835
pthread_mutex_lock(&A);
2936
__goblint_check(a <= 1);
3037
__goblint_check(b <= 2);
31-
__goblint_check(c <= 3);
38+
__goblint_check(c <= 4); // UNKNOWN!
3239
pthread_mutex_unlock(&A);
3340
return 0;
3441
}

0 commit comments

Comments
 (0)