update test cases

tests/regression/85-relational-malloc/04-global2.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --set ana.activated[+] apron  --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none   --enable ana.sv-comp.functions
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --set ana.activated[+] apron  --set ana.apron.domain polyhedra --set sem.int.signed_overflow assume_none --enable ana.sv-comp.functions --disable warn.integer
 #include <stdlib.h>
 extern int __VERIFIER_nondet_int(void);
 

tests/regression/85-relational-malloc/05-multi-thread.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] memOutOfBounds --set ana.activated[+] apron  --set ana.apron.domain polyhedra  --set ana.path_sens[+] threadflag   --set ana.activated[+] taintPartialContexts  --set ana.base.privatization mutex-meet-tid --set ana.activated[+] threadJoins --set ana.ctx_insens[+] threadJoins --enable ana.int.interval
+// PARAM: --set ana.activated[+] memOutOfBounds --set ana.activated[+] apron  --set ana.apron.domain polyhedra    --set ana.activated[+] taintPartialContexts --set ana.ctx_insens[+] threadJoins --enable ana.int.interval
 #include <stdlib.h>
 #include <pthread.h>
 
@@ -8,7 +8,8 @@ int *gptr;
 void *t_other(void *arg)
 {
     pthread_mutex_lock(&mtx);
-    int tmp = *gptr;     // WARN
+    // we loose all information about the relation between the ghost variables and the len after entering multithreaded context
+    int tmp = *gptr;     
     pthread_mutex_unlock(&mtx);
 }
 

tests/regression/85-relational-malloc/08-negative-indices.c

@@ -24,6 +24,5 @@ int main()
         }
         *(t + 1) = 2; // NOWARN
         *(t + i) = 2; // WARN
-        *(t+len) =2;
     }
 }

tests/regression/85-relational-malloc/09-casting.c

@@ -3,33 +3,38 @@
 #include <stdlib.h>
 #include <time.h>
 
-
 int main()
 {
 
     unsigned int len = rand();
 
-    int* p = malloc(sizeof(int) * len);
+    int *p = malloc(sizeof(int) * len);
 
-    char * t = p; 
-    for (int i = 0; i < sizeof(int) * len /sizeof(char); i++)
+    char *t = p;
+    for (int i = 0; i < sizeof(int) * len / sizeof(char); i++)
     {
-        *(t + i) = 2;
-        *(t+1) = 2;
-        char tmp = *(t + i);
+        *(t + i) = 2;        // NOWARN
+        *(t + 1) = 2;        // NOWARN
+        *(t + 2) = 2;        // NOWARN
+        *(t + 4) = 2;        // WARN
+        *(t - 1) = 2;        // WARN
+        char tmp = *(t + i); // NOWARN
     }
-    
+
     free(p);
 
     long *p = malloc(sizeof(long) * len);
 
-    int * t = p; 
-    for (int i = 0; i < sizeof(long)/sizeof(int) * len ; i++)
+    int *t = p;
+    for (int i = 0; i < sizeof(long) / sizeof(int) * len; i++)
     {
-        *(t + i) = 2;
-        *(t+1) = 2;
-        int tmp = *(t + i);
+        *(t + i) = 2;       // NOWARN
+        *(t + 1) = 2;       // NOWARN
+        *(t + 2) = 2;       // WARN
+        *(t + 4) = 2;       // WARN
+        *(t - 1) = 2;       // WARN
+        int tmp = *(t + i); // NOWARN
     }
-    
+
     free(p);
 }

tests/regression/85-relational-malloc/12-pointer-tracking-multi-thread.c

@@ -10,7 +10,8 @@ pthread_mutex_t mtx = PTHREAD_MUTEX_INITIALIZER;
 void *t_other(int *len)
 {
     pthread_mutex_lock(&mtx);
-    int tmp = *gptr;     // WARN
+    // we loose all information about the relation between the ghost variables and the len after entering multithreaded context
+    int tmp = *gptr;     
     pthread_mutex_unlock(&mtx);
 }
 

tests/regression/85-relational-malloc/13-global-pointer2.c

@@ -11,12 +11,12 @@ void *t_other()
     for (int i = 0; i < len; i++)
     {
         gptr[i] = 42;     // NOWARN
-        // gptr[i + 1] = 42; // WARN
-        // gptr[i - 1] = 42; // WARN
+        gptr[i + 1] = 42; // WARN
+        gptr[i - 1] = 42; // WARN
 
-        // int tmp = gptr[i];     // NOWARN
-        // int tmp = gptr[i + 1]; // WARN
-        // int tmp = gptr[i - 1]; // WARN
+        int tmp = gptr[i];     // NOWARN
+        int tmp = gptr[i + 1]; // WARN
+        int tmp = gptr[i - 1]; // WARN
     }
 }
 
@@ -30,13 +30,12 @@ int main()
     for (int i = 0; i < len; i++)
     {
         gptr[i] = 42;     // NOWARN
-        // gptr[i + 1] = 42; // WARN
-        // gptr[i - 1] = 42; // WARN
+        gptr[i + 1] = 42; // WARN
+        gptr[i - 1] = 42; // WARN
 
-        // int tmp = gptr[i];     // NOWARN
-        // int tmp = gptr[i + 1]; // WARN
-        // int tmp = gptr[i - 1]; // WARN
-        assert(i< len);
+        int tmp = gptr[i];     // NOWARN
+        int tmp = gptr[i + 1]; // WARN
+        int tmp = gptr[i - 1]; // WARN
     }
     free(gptr);
     return 0;

tests/regression/86-relational-array-oob/01-random-simple.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.arrayoob    --set ana.activated[+] apron   --set ana.apron.domain octagon --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.arrayoob    --set ana.activated[+] apron   --set ana.apron.domain octagon 
 
 
 #include <stdio.h>

tests/regression/86-relational-array-oob/03-simple-if-else.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.arrayoob --enable ana.int.interval   --set ana.activated[+] apron   --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.arrayoob --enable ana.int.interval   --set ana.activated[+] apron  
 
 int main()
 {

tests/regression/86-relational-array-oob/04-global.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.arrayoob --enable ana.int.interval   --set ana.activated[+] apron   --set sem.int.signed_overflow assume_none  --disable warn.integer
+// PARAM: --enable ana.arrayoob --enable ana.int.interval   --set ana.activated[+] apron   --disable warn.integer
 
 int readUntil(char arr[], unsigned len)
 {
@@ -29,7 +29,7 @@ int main()
         len = 10;
 
     char ptr[len];
-    readUntil(ptr, len);
+    readUntil(ptr+1, len);
 
     for (unsigned int i = 0; i < len; i++)
     {