aggressive slicer regression tests

Author: polgreen

regression/goto-instrument/aggressive_slicer1/main.c

@@ -0,0 +1,36 @@
+// test should pass. Shortest path main -> C -> D
+void D()
+{
+  __CPROVER_assert(0, "");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+    D();
+}
+
+void B()
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+
+  __CPROVER_assume(nondet != 3);
+  switch(nondet)
+  {
+  case 1:
+    B();
+    break;
+  case 3:
+    C();
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/goto-instrument/aggressive_slicer1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer2/main.c

@@ -0,0 +1,39 @@
+// test should pass. Shortest path is preserved, main -> C -> D,
+// but is not a possible counterexample because of assumption that
+// nondet != 3
+
+void D()
+{
+  __CPROVER_assert(0, "");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+    D();
+}
+
+void B()
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+
+  __CPROVER_assume(nondet != 3);
+  switch(nondet)
+  {
+  case 1:
+    B();
+    break;
+  case 3:
+    C();
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/goto-instrument/aggressive_slicer2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --property D.assertion.1
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer3/main.c

@@ -0,0 +1,35 @@
+// test should fail. Shortest path is preserved, main -> C -> D,
+void D()
+{
+  __CPROVER_assert(0, "");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+    D();
+}
+
+void B()
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+
+  switch(nondet)
+  {
+  case 1:
+    B();
+    break;
+  case 3:
+    C();
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/goto-instrument/aggressive_slicer3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer4/main.c

@@ -0,0 +1,39 @@
+// test should fail
+// shortest path only is not sufficient to violate assertion,
+// but we specifically require that function B is kept, which
+// allows path main -> B -> C -> D
+
+void D()
+{
+  __CPROVER_assert(0, "");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+    D();
+}
+
+void B()
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+  __CPROVER_assume(nondet != 3);
+  switch(nondet)
+  {
+  case 1:
+    B();
+    break;
+  case 3:
+    C();
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/goto-instrument/aggressive_slicer4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --aggressive-slice-preserve-function B
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer5/main.c

@@ -0,0 +1,38 @@
+// Test should fail. Shortest path only is not sufficient
+// due to assumption that nondet !=3, but
+// preserve-all-direct-paths preserves the path main -> B -> C -> D.
+
+void D()
+{
+  __CPROVER_assert(0, "");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+    D();
+}
+
+void B()
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+  __CPROVER_assume(nondet != 3);
+  switch(nondet)
+  {
+  case 1:
+    B();
+    break;
+  case 3:
+    C();
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/goto-instrument/aggressive_slicer5/test.binary

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --property D.assertion.1 --aggressive-slice-preserve-all-direct-paths
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer5/test.desc

@@ -0,0 +1,40 @@
+// Test should fail
+// Assertion in D is reachable when call depth of 1 is preserved,
+// Shortest path = main -> C -> D, which is not possible due to assumption
+// nondet!=3, but call depth 1 preserves the body of function B, which can also reach
+// C.
+
+void D()
+{
+  __CPROVER_assert(0, "");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+    D();
+}
+
+void B()
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+  __CPROVER_assume(nondet != 3);
+  switch(nondet)
+  {
+  case 1:
+    B();
+    break;
+  case 3:
+    C();
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/goto-instrument/aggressive_slicer6/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --aggressive-slice-call-depth 1
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer6/test.desc

@@ -0,0 +1,46 @@
+// Test should fail
+// Assertion in D is reachable by main -> C -> D
+// Assertion in E is reachable by main -> E
+
+void D()
+{
+  __CPROVER_assert(0, "");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+    D();
+}
+
+void B()
+{
+  C();
+};
+
+void E()
+{
+  __CPROVER_assert(0, "");
+}
+
+int main()
+{
+  int nondet;
+
+  switch(nondet)
+  {
+  case 1:
+    B();
+    break;
+  case 2:
+    E();
+    break;
+  case 3:
+    C();
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/goto-instrument/aggressive_slicer7/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring