Properly fixes test descriptions for contracts regression

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

…tracts/function-calls-03-1/test-enf.desc …cts/function-calls-03-1/test-enf-f1.descregression/contracts/function-calls-03-1/test-enf.desc renamed to regression/contracts/function-calls-03-1/test-enf-f1.desc regression/contracts/function-calls-03-1/test-enf.desc renamed to regression/contracts/function-calls-03-1/test-enf-f1.desc

@@ -0,0 +1,21 @@
+CORE
+main.c
+--enforce-contract f2 _ --unwind 20 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^file main.c line \d+ function f2: recursion is ignored on call to \'f2\'$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
+^\[f2.\d+\] line \d+ Check that loc is assignable: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  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-1/test-enf-f2.desc

@@ -14,7 +14,8 @@ Verification:
   f1       | assumed  | asserted
 
 Test should fail:
-The postcondition of f2 is incorrect, considering the recursion particularity. 
+The postcondition of f2_out 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).
+The base case for the recursive call to f2_out provides different behavior
+than the general case (given the pre-conditions).

…tracts/function-calls-04-1/test-enf.desc …cts/function-calls-04-1/test-enf-f1.descregression/contracts/function-calls-04-1/test-enf.desc renamed to regression/contracts/function-calls-04-1/test-enf-f1.desc regression/contracts/function-calls-04-1/test-enf.desc renamed to regression/contracts/function-calls-04-1/test-enf-f1.desc

@@ -0,0 +1,22 @@
+CORE
+main.c
+--enforce-contract f2_in _ --unwind 20 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^file main.c line \d+ function f2\_out: recursion is ignored on call to \'f2\_in\'$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
+^\[f2\_out.\d+\] line \d+ Check that loc2 is assignable: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f2_in    | assumed  | asserted
+
+Test should fail:
+The postcondition of f2_out is incorrect, considering the recursion particularity. 
+
+Recursion:
+The base case for the recursive call to f2_out provides different behavior
+than the general case (given the pre-conditions).

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

@@ -0,0 +1,22 @@
+CORE
+main.c
+--enforce-contract f2_out _ --unwind 20 --unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^file main.c line \d+ function f2\_in: recursion is ignored on call to \'f2\_out\'$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: FAILURE$
+^\[f2\_out.\d+\] line \d+ Check that loc2 is assignable: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f2_out   | 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_out provides different behavior
+than the general case (given the pre-conditions).