Split 82-widen/02-mihaila-widen-fig7-delay into two tests

goblint · Jun 7, 2024 · 1a8021d · 1a8021d
1 parent f34fc14
commit 1a8021d
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 2 deletions.
diff --git a/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c b/tests/regression/82-widen/02-mihaila-widen-fig7-delay.c
@@ -1,6 +1,5 @@
-// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 3
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --enable ana.sv-comp.functions --set ana.widen.delay.local 1
 // From "Widening as Abstract Domain", Fig. 7: https://doi.org/10.1007/978-3-642-38088-4_12
-// They claim delay 2 (https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf), we need 3 for some reason. Why?
 #include <goblint.h>
 extern _Bool __VERIFIER_nondet_bool();
 

diff --git a/tests/regression/82-widen/03-mihaila-widen-slide-delay.c b/tests/regression/82-widen/03-mihaila-widen-slide-delay.c
@@ -0,0 +1,19 @@
+// PARAM: --disable ana.int.def_exc --enable ana.int.interval --set ana.widen.delay.local 3
+// From "Widening as Abstract Domain" slides: https://bytebucket.org/mihaila/bindead/wiki/resources/widening-talk.pdf
+// They claim delay 2, we need 3 for some reason. Why?
+#include <goblint.h>
+
+int main() {
+  int x = 0;
+  int y = 0;
+  while (x < 100) {
+    __goblint_check(0 <= y);
+    __goblint_check(y <= 1);
+    if (x > 5)
+      y = 1;
+    x = x + 4;
+  }
+  __goblint_check(0 <= y);
+  __goblint_check(y <= 1);
+  return 0;
+}
diff --git a/tests/regression/82-widen/03-mine14-delay.c → tests/regression/82-widen/04-mine14-delay.c b/tests/regression/82-widen/03-mine14-delay.c → tests/regression/82-widen/04-mine14-delay.c