Changes to tests

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>

Author: michael-schwarz

tests/regression/85-narrow_globs/02-state-machine.c

@@ -1,5 +1,6 @@
 // PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled
-#include <stdlib.h>
+#include <pthread.h>
+#include <goblint.h>
 
 int state = 0;
 

tests/regression/85-narrow_globs/07-ctxt-widen.c

@@ -1,6 +1,6 @@
 // PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled
 // Taken from context gas tests, where the assertions were unknown.
-#include <stdio.h>
+#include <goblint.h>
 
 int h(int i)
 {

tests/regression/85-narrow_globs/08-ctxt-insensitive.c

@@ -1,10 +1,11 @@
 // PARAM: --set ana.context.callString_length 0 --set "ana.activated[+]" call_string --set ana.ctx_sens "['call_string']" --enable ana.int.interval_set --enable solvers.td3.narrow-globs.enabled
+#include <goblint.h>
 
 int fac(int i) {
     if (i > 0) {
         return fac(i - 1) * i;
     }
-    assert(i == 0);
+    __goblint_check(i == 0);
     return 1;
 }
 

tests/regression/85-narrow_globs/12-multiple-growing-updates.c

@@ -1,11 +1,12 @@
 // PARAM: --enable ana.int.interval_set --enable solvers.td3.narrow-globs.enabled
 #include <pthread.h>
+#include <goblint.h>
 
 pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
 int glob = 0;
 int glob2 = 0;
 
-void *thread(void *d) {    
+void *thread(void *d) {
     for(int i = 0; i < 10; i++) {
         pthread_mutex_lock(&mutex);
         glob = i;

tests/regression/85-narrow_globs/13-threaded-ctxt-widen.c

@@ -1,11 +1,12 @@
 // PARAM: --enable ana.int.interval_set --set ana.context.gas_value 0 --enable solvers.td3.narrow-globs.enabled
 #include <pthread.h>
+#include <goblint.h>
 
 pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
 int glob = 0;
 int glob2 = 0;
 
-void *thread(void *d) {    
+void *thread(void *d) {
     f(10);
     return NULL;
 }

tests/regression/85-narrow_globs/14-widening-thresholds.c

@@ -1,7 +1,7 @@
 // PARAM: --enable ana.int.interval --enable ana.int.interval_threshold_widening --set ana.int.interval_threshold_widening_constants comparisons --enable solvers.td3.narrow-globs.enabled
 #include <pthread.h>
+#include <goblint.h>
 
-//TODO: this tests that threshold widening also narrows correctly. This should not be in this folder
 pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
 int glob = 0;
 

tests/regression/85-narrow_globs/15-intertwined_increment.c

@@ -1,6 +1,6 @@
-// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled 
+// PARAM: --enable ana.int.interval --enable solvers.td3.narrow-globs.enabled
 #include <pthread.h>
-#include <stdio.h>
+#include <goblint.h>
 
 int a, b;
 pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;

tests/regression/85-narrow_globs/16-cyclic-dependency-guarded.c

@@ -1,6 +1,5 @@
 // PARAM: --enable solvers.td3.narrow-globs.enabled --set solvers.td3.narrow-globs.narrow-gas 9 --enable ana.int.interval --set ana.base.privatization protection-read  --enable ana.base.priv.protection.changes-only
-
-// This is supposed to check if the solver terminates
+// NOTIMEOUT
 #include <pthread.h>
 #include <goblint.h>
 
@@ -32,4 +31,4 @@ int main(void) {
   __goblint_check(b <= 10);
   pthread_mutex_unlock(&mutex);
   return 0;
-}
+}