Add test case with invalid deref in complex loop

goblint · Oct 3, 2023 · 9d64db1 · 9d64db1
1 parent fb4ad24
commit 9d64db1
Showing 1 changed file with 20 additions and 0 deletions.
diff --git a/tests/regression/77-mem-oob/10-oob-two-loops.c 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;
+}