aggressive slicer regression tests

Author: polgreen

regression/goto-instrument/aggressive_slicer1/main.c

@@ -0,0 +1,30 @@
+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,30 @@
+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,29 @@
+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,29 @@
+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 --preserve-function B
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer5/main.c

@@ -0,0 +1,29 @@
+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,29 @@
+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 --call-depth 1
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring