Adds code contracts regression tests that involve function calls

regression/contracts/chain.sh

@@ -11,6 +11,14 @@ name=${*:$#}
 name=${name%.c}
 
 args=${*:5:$#-5}
+if [[ "$args" != *" _ "* ]]
+then
+  args_inst=$args
+  args_cbmc=""
+else
+  args_inst="${args%%" _ "*}"
+  args_cbmc="${args#*" _ "}"
+fi
 
 if [[ "${is_windows}" == "true" ]]; then
   $goto_cc "${name}.c"
@@ -20,10 +28,10 @@ else
 fi
 
 rm -f "${name}-mod.gb"
-$goto_instrument ${args} "${name}.gb" "${name}-mod.gb"
+$goto_instrument ${args_inst} "${name}.gb" "${name}-mod.gb"
 if [ ! -e "${name}-mod.gb" ] ; then
   cp "$name.gb" "${name}-mod.gb"
-elif echo $args | grep -q -- "--dump-c" ; then
+elif echo $args_inst | grep -q -- "--dump-c" ; then
   mv "${name}-mod.gb" "${name}-mod.c"
 
   if [[ "${is_windows}" == "true" ]]; then
@@ -36,4 +44,4 @@ elif echo $args | grep -q -- "--dump-c" ; then
   rm "${name}-mod.c"
 fi
 $goto_instrument --show-goto-functions "${name}-mod.gb"
-$cbmc "${name}-mod.gb"
+$cbmc "${name}-mod.gb" ${args_cbmc}

regression/contracts/function-calls-01/main.c

@@ -0,0 +1,14 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 1)
+{
+  return *x1 + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 1 && p < 10000);
+  f1(&p);
+
+  return 0;
+}

regression/contracts/function-calls-01/test-enf.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted

regression/contracts/function-calls-01/test-rep.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed

regression/contracts/function-calls-02-1/main.c

@@ -0,0 +1,21 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 3)
+{
+  int loc = *x1 + 1;
+  return f2(&loc) + 1;
+}
+
+int f2(int *x2) __CPROVER_requires(*x2 > 2 && *x2 < 10001)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  return *x2 + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 1 && p < 10000);
+  f1(&p);
+
+  return 0;
+}

regression/contracts/function-calls-02-1/test-enf.desc

@@ -0,0 +1,16 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.

regression/contracts/function-calls-02-1/test-mix.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | asserted | assumed

regression/contracts/function-calls-02-1/test-rep.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed
+  f2       | n/a      | n/a
+
+Note: the call to f2 does not occur because the call to f1 is replaced by its contracts.

regression/contracts/function-calls-02/main.c

@@ -0,0 +1,20 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
+{
+  return f2(x1) + 1;
+}
+
+int f2(int *x2) __CPROVER_requires(*x2 > 1 && *x2 < 10000)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  return *x2 + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 1 && p < 10000);
+  f1(&p);
+
+  return 0;
+}

regression/contracts/function-calls-02/test-enf.desc

@@ -0,0 +1,16 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.

regression/contracts/function-calls-02/test-mix.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | asserted | assumed

regression/contracts/function-calls-02/test-rep.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed
+  f2       | n/a      | n/a
+
+Note: the call to f2 does not occur because the call to f1 is replaced by its contracts.

regression/contracts/function-calls-03-1/main.c

@@ -0,0 +1,23 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
+{
+  return f2(x1) + 1;
+}
+
+int f2(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  if(*x2 < 1)
+    return -1; //Notice the change for the base case
+  int loc = *x2 - 1;
+  return f2(&loc) + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 0 && p < 20);
+  f1(&p);
+
+  return 0;
+}

regression/contracts/function-calls-03-1/test-enf.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
+
+Test should fail:
+The postcondition of f2 is incorrect, considering the recursion particularity. 
+
+Recursion:
+The base case for the recursive call to f2 provides different behavior than the common case (given the pre-conditions).

regression/contracts/function-calls-03/main.c

@@ -0,0 +1,23 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
+{
+  return f2(x1) + 1;
+}
+
+int f2(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  if(*x2 < 1)
+    return 1;
+  int loc = *x2 - 1;
+  return f2(&loc) + 1;
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 0 && p < 20);
+  f1(&p);
+
+  return 0;
+}

regression/contracts/function-calls-03/test-enf.desc

@@ -0,0 +1,19 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.

regression/contracts/function-calls-03/test-mix.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | asserted | assumed
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).

regression/contracts/function-calls-03/test-rep.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed
+  f2       | n/a      | n/a
+
+Note: the call to f2 does not occur because the call to f1 is replaced by its contracts.
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).

regression/contracts/function-calls-04-1/main.c

@@ -0,0 +1,29 @@
+int f1(int *x1) __CPROVER_requires(*x1 > 0 && *x1 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x1 + 2)
+{
+  return f2_out(x1) + 1;
+}
+
+int f2_out(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  if(*x2 < 1)
+    return -1; //Notice the change for the base case
+  int loc2 = *x2 - 1;
+  return f2_in(&loc2) + 1;
+}
+
+int f2_in(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 19)
+  __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
+{
+  return f2_out(x2);
+}
+
+int main()
+{
+  int p;
+  __CPROVER_assume(p > 0 && p < 20);
+  f1(&p);
+
+  return 0;
+}

regression/contracts/function-calls-04-1/test-enf.desc

@@ -0,0 +1,20 @@
+CORE
+main.c
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2_out   | assumed  | asserted
+  f2_in    | assumed  | asserted
+
+Test should fail:
+The postcondition of f2 is incorrect, considering the recursion particularity. 
+
+Recursion:
+The base case for the recursive call to f2 provides different behavior than the general case (given the pre-conditions).