diff --git a/tests/regression/85-relational-malloc/04-global2.c b/tests/regression/85-relational-malloc/04-global2.c index 4458546794c..a49084c230e 100644 --- a/tests/regression/85-relational-malloc/04-global2.c +++ b/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 extern int __VERIFIER_nondet_int(void); diff --git a/tests/regression/85-relational-malloc/05-multi-thread.c b/tests/regression/85-relational-malloc/05-multi-thread.c index 68ea653f6bc..380cc69b302 100644 --- a/tests/regression/85-relational-malloc/05-multi-thread.c +++ b/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 #include @@ -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); } diff --git a/tests/regression/85-relational-malloc/08-negative-indices.c b/tests/regression/85-relational-malloc/08-negative-indices.c index d4a09789317..71043b7e9d2 100644 --- a/tests/regression/85-relational-malloc/08-negative-indices.c +++ b/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; } } diff --git a/tests/regression/85-relational-malloc/09-casting.c b/tests/regression/85-relational-malloc/09-casting.c index 4d2fc0fc81d..8b676e26c36 100644 --- a/tests/regression/85-relational-malloc/09-casting.c +++ b/tests/regression/85-relational-malloc/09-casting.c @@ -3,33 +3,38 @@ #include #include - 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); } diff --git a/tests/regression/85-relational-malloc/12-pointer-tracking-multi-thread.c b/tests/regression/85-relational-malloc/12-pointer-tracking-multi-thread.c index 0cedcdc8b2d..2688d11afed 100644 --- a/tests/regression/85-relational-malloc/12-pointer-tracking-multi-thread.c +++ b/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); } diff --git a/tests/regression/85-relational-malloc/13-global-pointer2.c b/tests/regression/85-relational-malloc/13-global-pointer2.c index 0def1156c90..7c6f8de3915 100644 --- a/tests/regression/85-relational-malloc/13-global-pointer2.c +++ b/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; diff --git a/tests/regression/86-relational-array-oob/01-random-simple.c b/tests/regression/86-relational-array-oob/01-random-simple.c index 724fb48696c..681ac269b5b 100644 --- a/tests/regression/86-relational-array-oob/01-random-simple.c +++ b/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 diff --git a/tests/regression/86-relational-array-oob/03-simple-if-else.c b/tests/regression/86-relational-array-oob/03-simple-if-else.c index 00befcb0abd..deb202d1fe4 100644 --- a/tests/regression/86-relational-array-oob/03-simple-if-else.c +++ b/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() { diff --git a/tests/regression/86-relational-array-oob/04-global.c b/tests/regression/86-relational-array-oob/04-global.c index 486b71f4b1c..e89efc14e0f 100644 --- a/tests/regression/86-relational-array-oob/04-global.c +++ b/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++) {