rename folder numbers from 99 98 to 86 85

tests/regression/46-apron2/59-no-overflow.c

@@ -0,0 +1,14 @@
+// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron
+// This test checks the no overflow computation in apron
+int main()
+{
+    unsigned int len = rand();
+    len = len % 10;
+    int top;
+    for (int i = 0; 1 - (i - 1 < len) < 1; i++) // raises both both branch dead if no_overflow is wrong computed
+    {
+        int tmp = i;
+    }
+
+    return 0;
+}

tests/regression/97-relational-malloc/01-random-simples.c → tests/regression/85-relational-malloc/01-random-simples.c

@@ -1,18 +1,18 @@
-// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --set ana.activated[+] apron  --set ana.apron.domain polyhedra
+// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval --set ana.activated[+] apron  --set ana.apron.domain polyhedra 
+
 #include <stdlib.h>
 
+char *arr;
 int main()
 {
-    int len = rand();
+    unsigned int len = rand();
 
-    char *arr;
     arr = malloc(sizeof(char) * len);
 
-    for (int i = 0; i < len; i++)
+    for (int i = 0; (unsigned int)i < len; i++)
     {
-        char tmp = *(arr);   // NOWARN
-        arr[i] = 42;     // NOWARN
+        arr[i] = 42;      // NOWARN
         arr[i + 1] = 127; // WARN
-        arr[i - 1] = 42; // WARN
+        arr[i - 1] = 42;  // WARN
     }
 }

tests/regression/97-relational-malloc/04-global2.c → 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 --disable warn.info --disable sem.unknown_function.invalidate.globals
+// 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
 #include <stdlib.h>
 extern int __VERIFIER_nondet_int(void);
 
@@ -10,7 +10,7 @@ int test_fun(int a[], int N)
   {
     while (a[i] > 0) // NOWARN
     {
-      a[i]--;
+      a[i]--; // NOWARN
       res++;
     }
   }

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

@@ -1,25 +1,25 @@
-// PARAM: --set ana.activated[+] memOutOfBounds --set ana.activated[+] apron  --set ana.apron.domain polyhedra  --set ana.activated[+] threadJoins  --set ana.path_sens[+] threadflag  --set ana.base.privatization mutex-meet-tid
+// 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
 #include <stdlib.h>
-#include <stdio.h>
 #include <pthread.h>
 
 pthread_mutex_t mtx = PTHREAD_MUTEX_INITIALIZER;
 
-void *t_other(int *gptr)
+int *gptr;
+void *t_other(void *arg)
 {
     pthread_mutex_lock(&mtx);
-    int tmp = *gptr; // TODO analysis does not work with escaped/global len variable
+    int tmp = *gptr;     // WARN
     pthread_mutex_unlock(&mtx);
 }
 
 int main()
 {
     int len = rand();
     len %= 10;
-    int*  gptr = malloc(sizeof(int) * len);
+    gptr = malloc(sizeof(int) * len);
 
     pthread_t thread;
-    pthread_create(&thread, NULL, t_other, gptr);
+    pthread_create(&thread, NULL, t_other, NULL);
 
     pthread_mutex_lock(&mtx);
     for (int i = 0; i < len; i++)

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

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

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

@@ -0,0 +1,44 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --set ana.activated[+] threadJoins --set ana.activated[+] apron  --set ana.apron.domain polyhedra --enable ana.int.interval --set ana.activated[+] taintPartialContexts  --set ana.activated[+] thread  --enable ana.apron.pointer_tracking --set sem.int.signed_overflow assume_none  --disable warn.integer
+#include <stdlib.h>
+#include <stdio.h>
+#include <pthread.h>
+
+int *gptr;
+
+pthread_mutex_t mtx = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_other(int *len)
+{
+    pthread_mutex_lock(&mtx);
+    int tmp = *gptr;     // WARN
+    pthread_mutex_unlock(&mtx);
+}
+
+int main()
+{
+    int len = rand();
+    len %= 10;
+    gptr = malloc(sizeof(int) * len);
+
+    pthread_t thread;
+    pthread_create(&thread, NULL, t_other, NULL);
+
+    pthread_mutex_lock(&mtx);
+    int x = 0;
+    int *p = gptr;
+    while (x < len)
+    {
+        *p = 42;       // NOWARN
+        *(p + 1) = 42; // WARN
+
+        int tmp = *p;   // NOWARN
+        tmp = *(p - 1); // WARN
+        p++;
+        x++;
+    }
+    pthread_mutex_unlock(&mtx);
+
+    pthread_join(thread, NULL);
+    free(gptr);
+    return 0;
+}

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

@@ -0,0 +1,43 @@
+// PARAM: --set ana.activated[+] memOutOfBounds --set ana.activated[+] taintPartialContexts  --set ana.activated[+] apron  --set ana.apron.domain polyhedra  --set ana.activated[+] allocVarEscaped --enable ana.int.interval
+#include <stdlib.h>
+#include <stdio.h>
+#include <pthread.h>
+
+int len;
+int *gptr;
+
+void *t_other()
+{
+    for (int i = 0; i < len; i++)
+    {
+        gptr[i] = 42;     // NOWARN
+        // 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 main()
+{
+    len = rand();
+    len %= 10;
+    gptr = malloc(sizeof(int) * len);
+
+    t_other();
+    for (int i = 0; i < len; i++)
+    {
+        gptr[i] = 42;     // NOWARN
+        // 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);
+    }
+    free(gptr);
+    return 0;
+}

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

@@ -1,4 +1,5 @@
-// PARAM: --enable ana.arrayoob    --set ana.activated[+] apron   --set ana.apron.domain octagon
+// PARAM: --enable ana.arrayoob    --set ana.activated[+] apron   --set ana.apron.domain octagon --set sem.int.signed_overflow assume_none
+
 
 #include <stdio.h>
 #include <stdlib.h>
@@ -7,7 +8,7 @@
 int main()
 {
     srand(time(NULL));
-    unsigned int len = (rand() % 32) + 3;
+     int len = (rand() % 32) + 3;
     char arr[len];
 
     for (int i = 0; i < len; i++)

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

@@ -30,4 +30,19 @@ int main()
 
     char ptr[len];
     readUntil(ptr, len);
+
+    for (unsigned int i = 0; i < len; i++)
+    {
+        char s = ptr[i];     // NOWARN
+        char s = ptr[i - 1]; // WARN
+        char s = ptr[i + 1]; // WARN
+        char s = ptr[i - i]; // NOWARN
+        char s = ptr[i + i]; // WARN
+
+        ptr[i] = 42;      // NOWARN
+        ptr[i - 1] = 42;  // WARN
+        ptr[i + 1] = -42; // WARN
+        ptr[i - i] = -42; // NOWARN
+        ptr[i + i] = -42; // WARN
+    }
 }