Assesses PR comments and adds handling for loop unwinding

Author: Aren Babikian

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/test-enf.desc

@@ -6,4 +6,7 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the postconditions.
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted

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

@@ -6,4 +6,7 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the preconditions.
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | asserted | assumed

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

@@ -6,8 +6,11 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the postconditions of both f1 and f2.
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
 
 Known bug:
 Enforce flag not handled correctly for function calls within functions.
-This bug is fixed in PR #5538.

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

@@ -6,4 +6,8 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the preconditions of f2 (called from f1) and of the postcondition of f1.
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | asserted | assumed

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

@@ -6,4 +6,10 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the preconditions of f1 (called from main).
+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/test-enf.desc

@@ -6,8 +6,11 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the postconditions of both f1 and f2.
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | assumed  | asserted
 
 Known bug:
 Enforce flag not handled correctly for function calls within functions.
-This bug is fixed in PR #5538.

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

@@ -6,4 +6,8 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the preconditions of f2 (called from f1) and of the postcondition of f1.
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2       | asserted | assumed

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

@@ -6,4 +6,10 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the preconditions of f1 (called from main).
+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/test-enf.desc

@@ -1,18 +1,19 @@
-KNOWNBUG
+CORE
 main.c
---enforce-all-contracts
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 --
-This confirms the accuracy of the postconditions of both f1 and f2. 
+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).
-
-Known bug 2:
-This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.