From 9d64db11a69abf60b0c777ee591860416c49666d Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Tue, 3 Oct 2023 16:33:09 +0200 Subject: [PATCH] Add test case with invalid deref in complex loop --- .../regression/77-mem-oob/10-oob-two-loops.c | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 tests/regression/77-mem-oob/10-oob-two-loops.c diff --git a/tests/regression/77-mem-oob/10-oob-two-loops.c b/tests/regression/77-mem-oob/10-oob-two-loops.c new file mode 100644 index 0000000000..2661f3dff7 --- /dev/null +++ b/tests/regression/77-mem-oob/10-oob-two-loops.c @@ -0,0 +1,20 @@ +// PARAM: --set ana.activated[+] memOutOfBounds --enable ana.int.interval +int main() { + int *p = malloc(1048 * sizeof(int)); + + for (int i = 0; i < 1048; ++i) { + p[i] = __VERIFIER_nondet_int(); //NOWARN + } + + int *q = p; + + while (*q >= 0 && q < p + 1048 * sizeof(int)) { //WARN + if (__VERIFIER_nondet_int()) { + q++; + } else { + (*q)--; //WARN + } + } + free(p); + return 0; +}