Regression tests for make-function-assume-false

Author: polgreen

regression/goto-instrument/make_function_assume_false1/main.c

@@ -0,0 +1,10 @@
+void function_a()
+{
+  __CPROVER_assert(0,"");
+}
+
+int main()
+{
+  function_a();
+  return 0;
+}

regression/goto-instrument/make_function_assume_false1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--make-function-assume-false function_a
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/make_function_assume_false2/main.c

@@ -0,0 +1,13 @@
+void function_a(int *num)
+{
+ *num = *num+1;
+}
+
+int main()
+{
+  int b=0;
+  int c;
+  if(c)
+    function_a(&b);
+  __CPROVER_assert(b==0, "");
+}

regression/goto-instrument/make_function_assume_false2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--make-function-assume-false function_a
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/make_function_assume_false3/main.c

@@ -0,0 +1,13 @@
+void function_a(int *num)
+{
+ *num = *num+1;
+}
+
+int main()
+{
+  int b=0;
+  int c;
+  if(c)
+    function_a(&b);
+  __CPROVER_assert(b!=0, "");
+}

regression/goto-instrument/make_function_assume_false3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--make-function-assume-false function_a
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring