Add regression tests for pre and postconditions

Author: angelhof

regression/cbmc/cprover_postcondition/main.c

@@ -0,0 +1,14 @@
+int func(int a)
+{
+  __CPROVER_precondition(a > 10, "Argument should be larger than 10");
+  int rval = a - 10;
+  __CPROVER_postcondition(rval > 1, "Return value should be positive");
+  return rval;
+}
+
+int main()
+{
+  int a = 11;
+  int rval = func(a);
+  return 0;
+}

regression/cbmc/cprover_postcondition/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--

regression/cbmc/cprover_precondition/main.c

@@ -0,0 +1,13 @@
+void func(int a)
+{
+  __CPROVER_precondition(a > 10, "Argument should be larger than 10.");
+}
+
+int main()
+{
+  int a = 10;
+
+  func(a);
+
+  return 0;
+}

regression/cbmc/cprover_precondition/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--