From 2928600a967d9a7882b147f8855f981ab47c7e5c Mon Sep 17 00:00:00 2001
From: Aren Babikian
 <babikian@dev-dsk-babikian-1d-e8327e0f.us-east-1.amazon.com>
Date: Wed, 10 Mar 2021 20:08:46 +0000
Subject: [PATCH 1/6] Adds regression tests that involve non-recursive function
 calls

---
 regression/contracts/function-calls-01/main.c | 15 ++++++++++++
 .../contracts/function-calls-01/test-enf.desc |  9 ++++++++
 .../contracts/function-calls-01/test-rep.desc |  9 ++++++++
 .../contracts/function-calls-02-1/main.c      | 23 +++++++++++++++++++
 .../function-calls-02-1/test-enf.desc         | 13 +++++++++++
 .../function-calls-02-1/test-mix.desc         |  9 ++++++++
 .../function-calls-02-1/test-rep.desc         |  9 ++++++++
 regression/contracts/function-calls-02/main.c | 22 ++++++++++++++++++
 .../contracts/function-calls-02/test-enf.desc | 13 +++++++++++
 .../contracts/function-calls-02/test-mix.desc |  9 ++++++++
 .../contracts/function-calls-02/test-rep.desc |  9 ++++++++
 11 files changed, 140 insertions(+)
 create mode 100644 regression/contracts/function-calls-01/main.c
 create mode 100644 regression/contracts/function-calls-01/test-enf.desc
 create mode 100644 regression/contracts/function-calls-01/test-rep.desc
 create mode 100644 regression/contracts/function-calls-02-1/main.c
 create mode 100644 regression/contracts/function-calls-02-1/test-enf.desc
 create mode 100644 regression/contracts/function-calls-02-1/test-mix.desc
 create mode 100644 regression/contracts/function-calls-02-1/test-rep.desc
 create mode 100644 regression/contracts/function-calls-02/main.c
 create mode 100644 regression/contracts/function-calls-02/test-enf.desc
 create mode 100644 regression/contracts/function-calls-02/test-mix.desc
 create mode 100644 regression/contracts/function-calls-02/test-rep.desc

diff --git a/regression/contracts/function-calls-01/main.c b/regression/contracts/function-calls-01/main.c
new file mode 100644
index 00000000000..09ca17fc558
--- /dev/null
+++ b/regression/contracts/function-calls-01/main.c
@@ -0,0 +1,15 @@
+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;
+}
diff --git a/regression/contracts/function-calls-01/test-enf.desc b/regression/contracts/function-calls-01/test-enf.desc
new file mode 100644
index 00000000000..b2d6674d02a
--- /dev/null
+++ b/regression/contracts/function-calls-01/test-enf.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the postconditions.
diff --git a/regression/contracts/function-calls-01/test-rep.desc b/regression/contracts/function-calls-01/test-rep.desc
new file mode 100644
index 00000000000..4775f50bbb6
--- /dev/null
+++ b/regression/contracts/function-calls-01/test-rep.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions.
diff --git a/regression/contracts/function-calls-02-1/main.c b/regression/contracts/function-calls-02-1/main.c
new file mode 100644
index 00000000000..a6aeae94a8e
--- /dev/null
+++ b/regression/contracts/function-calls-02-1/main.c
@@ -0,0 +1,23 @@
+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;
+}
\ No newline at end of file
diff --git a/regression/contracts/function-calls-02-1/test-enf.desc b/regression/contracts/function-calls-02-1/test-enf.desc
new file mode 100644
index 00000000000..589e5fcce21
--- /dev/null
+++ b/regression/contracts/function-calls-02-1/test-enf.desc
@@ -0,0 +1,13 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the postconditions of both f1 and f2.
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.
+This bug is fixed in PR #5538.
diff --git a/regression/contracts/function-calls-02-1/test-mix.desc b/regression/contracts/function-calls-02-1/test-mix.desc
new file mode 100644
index 00000000000..f0c8b6818c0
--- /dev/null
+++ b/regression/contracts/function-calls-02-1/test-mix.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions of f2 (called from f1) and of the postcondition of f1.
diff --git a/regression/contracts/function-calls-02-1/test-rep.desc b/regression/contracts/function-calls-02-1/test-rep.desc
new file mode 100644
index 00000000000..c3b2440cb07
--- /dev/null
+++ b/regression/contracts/function-calls-02-1/test-rep.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions of f1 (called from main).
diff --git a/regression/contracts/function-calls-02/main.c b/regression/contracts/function-calls-02/main.c
new file mode 100644
index 00000000000..560695c0856
--- /dev/null
+++ b/regression/contracts/function-calls-02/main.c
@@ -0,0 +1,22 @@
+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;
+}
diff --git a/regression/contracts/function-calls-02/test-enf.desc b/regression/contracts/function-calls-02/test-enf.desc
new file mode 100644
index 00000000000..dbb61c76c65
--- /dev/null
+++ b/regression/contracts/function-calls-02/test-enf.desc
@@ -0,0 +1,13 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the postconditions of both f1 and f2.
+
+Known bug:
+Enforce flag not handled correctly for function calls within functions.
+This bug is fixed in PR #5583.
diff --git a/regression/contracts/function-calls-02/test-mix.desc b/regression/contracts/function-calls-02/test-mix.desc
new file mode 100644
index 00000000000..f0c8b6818c0
--- /dev/null
+++ b/regression/contracts/function-calls-02/test-mix.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions of f2 (called from f1) and of the postcondition of f1.
diff --git a/regression/contracts/function-calls-02/test-rep.desc b/regression/contracts/function-calls-02/test-rep.desc
new file mode 100644
index 00000000000..c3b2440cb07
--- /dev/null
+++ b/regression/contracts/function-calls-02/test-rep.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions of f1 (called from main).

From 3f2d21ec3c3b639c3483f7a8faf79f4ad5692b73 Mon Sep 17 00:00:00 2001
From: Aren Babikian
 <babikian@dev-dsk-babikian-1d-e8327e0f.us-east-1.amazon.com>
Date: Wed, 10 Mar 2021 20:19:08 +0000
Subject: [PATCH 2/6] Fixes PR number

---
 regression/contracts/function-calls-02/test-enf.desc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/regression/contracts/function-calls-02/test-enf.desc b/regression/contracts/function-calls-02/test-enf.desc
index dbb61c76c65..589e5fcce21 100644
--- a/regression/contracts/function-calls-02/test-enf.desc
+++ b/regression/contracts/function-calls-02/test-enf.desc
@@ -10,4 +10,4 @@ This confirms the accuracy of the postconditions of both f1 and f2.
 
 Known bug:
 Enforce flag not handled correctly for function calls within functions.
-This bug is fixed in PR #5583.
+This bug is fixed in PR #5538.

From 1b13a25591974f0f920e4b63a15b953f1b359e68 Mon Sep 17 00:00:00 2001
From: Aren Babikian
 <babikian@dev-dsk-babikian-1d-e8327e0f.us-east-1.amazon.com>
Date: Wed, 10 Mar 2021 20:59:57 +0000
Subject: [PATCH 3/6] Adds regression tests that involve recursive function
 calls

---
 .../contracts/function-calls-03-1/main.c      | 24 +++++++++++++++++++
 .../function-calls-03-1/test-enf.desc         | 18 ++++++++++++++
 regression/contracts/function-calls-03/main.c | 24 +++++++++++++++++++
 .../contracts/function-calls-03/test-enf.desc | 19 +++++++++++++++
 .../contracts/function-calls-03/test-mix.desc | 12 ++++++++++
 .../contracts/function-calls-03/test-rep.desc | 12 ++++++++++
 6 files changed, 109 insertions(+)
 create mode 100644 regression/contracts/function-calls-03-1/main.c
 create mode 100644 regression/contracts/function-calls-03-1/test-enf.desc
 create mode 100644 regression/contracts/function-calls-03/main.c
 create mode 100644 regression/contracts/function-calls-03/test-enf.desc
 create mode 100644 regression/contracts/function-calls-03/test-mix.desc
 create mode 100644 regression/contracts/function-calls-03/test-rep.desc

diff --git a/regression/contracts/function-calls-03-1/main.c b/regression/contracts/function-calls-03-1/main.c
new file mode 100644
index 00000000000..f0df8a62097
--- /dev/null
+++ b/regression/contracts/function-calls-03-1/main.c
@@ -0,0 +1,24 @@
+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;
+}
diff --git a/regression/contracts/function-calls-03-1/test-enf.desc b/regression/contracts/function-calls-03-1/test-enf.desc
new file mode 100644
index 00000000000..ec16ceefc94
--- /dev/null
+++ b/regression/contracts/function-calls-03-1/test-enf.desc
@@ -0,0 +1,18 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This confirms the accuracy of the postconditions of both f1 and f2. 
+
+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.
diff --git a/regression/contracts/function-calls-03/main.c b/regression/contracts/function-calls-03/main.c
new file mode 100644
index 00000000000..4f466a3b891
--- /dev/null
+++ b/regression/contracts/function-calls-03/main.c
@@ -0,0 +1,24 @@
+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;
+}
diff --git a/regression/contracts/function-calls-03/test-enf.desc b/regression/contracts/function-calls-03/test-enf.desc
new file mode 100644
index 00000000000..0ee5122b46b
--- /dev/null
+++ b/regression/contracts/function-calls-03/test-enf.desc
@@ -0,0 +1,19 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the postconditions of both f1 and f2.
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
+
+Known bug 1:
+Enforce flag not handled correctly for function calls within functions.
+This bug is fixed in PR #5538.
+
+Known bug 2:
+This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.
diff --git a/regression/contracts/function-calls-03/test-mix.desc b/regression/contracts/function-calls-03/test-mix.desc
new file mode 100644
index 00000000000..06afa685d2a
--- /dev/null
+++ b/regression/contracts/function-calls-03/test-mix.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions of f2 (called from f1) and of the postcondition of f1.
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
diff --git a/regression/contracts/function-calls-03/test-rep.desc b/regression/contracts/function-calls-03/test-rep.desc
new file mode 100644
index 00000000000..6c3eba4ffbe
--- /dev/null
+++ b/regression/contracts/function-calls-03/test-rep.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions of f1 (called from main).
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).

From 08660bfffef810960315ef3ff672c42ce4e9cf2e Mon Sep 17 00:00:00 2001
From: Aren Babikian
 <babikian@dev-dsk-babikian-1d-e8327e0f.us-east-1.amazon.com>
Date: Wed, 10 Mar 2021 21:00:47 +0000
Subject: [PATCH 4/6] Adds regression tests that involve alternate recursive
 function calls

---
 .../contracts/function-calls-04-1/main.c      | 31 +++++++++++++++++++
 .../function-calls-04-1/test-enf.desc         | 18 +++++++++++
 regression/contracts/function-calls-04/main.c | 31 +++++++++++++++++++
 .../contracts/function-calls-04/test-enf.desc | 19 ++++++++++++
 .../function-calls-04/test-mix-1.desc         | 12 +++++++
 .../function-calls-04/test-mix-2.desc         | 18 +++++++++++
 .../contracts/function-calls-04/test-rep.desc | 12 +++++++
 7 files changed, 141 insertions(+)
 create mode 100644 regression/contracts/function-calls-04-1/main.c
 create mode 100644 regression/contracts/function-calls-04-1/test-enf.desc
 create mode 100644 regression/contracts/function-calls-04/main.c
 create mode 100644 regression/contracts/function-calls-04/test-enf.desc
 create mode 100644 regression/contracts/function-calls-04/test-mix-1.desc
 create mode 100644 regression/contracts/function-calls-04/test-mix-2.desc
 create mode 100644 regression/contracts/function-calls-04/test-rep.desc

diff --git a/regression/contracts/function-calls-04-1/main.c b/regression/contracts/function-calls-04-1/main.c
new file mode 100644
index 00000000000..a5b160f3f87
--- /dev/null
+++ b/regression/contracts/function-calls-04-1/main.c
@@ -0,0 +1,31 @@
+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;
+}
diff --git a/regression/contracts/function-calls-04-1/test-enf.desc b/regression/contracts/function-calls-04-1/test-enf.desc
new file mode 100644
index 00000000000..4a3da990e58
--- /dev/null
+++ b/regression/contracts/function-calls-04-1/test-enf.desc
@@ -0,0 +1,18 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This confirms the accuracy of the postconditions of f1, f2_out and f2_in.
+
+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).
+
+Known bug:
+This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.
diff --git a/regression/contracts/function-calls-04/main.c b/regression/contracts/function-calls-04/main.c
new file mode 100644
index 00000000000..d9876b4e89c
--- /dev/null
+++ b/regression/contracts/function-calls-04/main.c
@@ -0,0 +1,31 @@
+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;
+  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;
+}
diff --git a/regression/contracts/function-calls-04/test-enf.desc b/regression/contracts/function-calls-04/test-enf.desc
new file mode 100644
index 00000000000..1969af0f946
--- /dev/null
+++ b/regression/contracts/function-calls-04/test-enf.desc
@@ -0,0 +1,19 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the postconditions of f1, f2_out and f2_in.
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
+
+Known bug 1:
+Enforce flag not handled correctly for function calls within functions.
+This bug is fixed in PR #5538.
+
+Known bug 2:
+This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.
diff --git a/regression/contracts/function-calls-04/test-mix-1.desc b/regression/contracts/function-calls-04/test-mix-1.desc
new file mode 100644
index 00000000000..c7e87562c3c
--- /dev/null
+++ b/regression/contracts/function-calls-04/test-mix-1.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-contract f1 --replace-call-with-contract f2_out
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions of f2_out (called from f1) and of the postconditions of f1.
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
diff --git a/regression/contracts/function-calls-04/test-mix-2.desc b/regression/contracts/function-calls-04/test-mix-2.desc
new file mode 100644
index 00000000000..01430c7905e
--- /dev/null
+++ b/regression/contracts/function-calls-04/test-mix-2.desc
@@ -0,0 +1,18 @@
+KNOWNBUG
+main.c
+--enforce-contract f1 --enforce-contract f2_out --replace-call-with-contract f2_in
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions of f2_in (called from f2_out) and of the postconditions of f1 and of f2_out.
+
+Recursion
+(1) This test checks the mutualy recursive f2_out and f2-in functions by enforcing f2_out and replacing the internal f2_in call with its contract.
+(2) This test does not require unwinding.
+(3) 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.
+This bug is fixed in PR #5538.
diff --git a/regression/contracts/function-calls-04/test-rep.desc b/regression/contracts/function-calls-04/test-rep.desc
new file mode 100644
index 00000000000..6c3eba4ffbe
--- /dev/null
+++ b/regression/contracts/function-calls-04/test-rep.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This confirms the accuracy of the preconditions of f1 (called from main).
+
+Recursion:
+The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).

From 7166cd592b35d42aadd0eced76ba01290d111c1a Mon Sep 17 00:00:00 2001
From: Aren Babikian
 <babikian@dev-dsk-babikian-1d-e8327e0f.us-east-1.amazon.com>
Date: Thu, 11 Mar 2021 04:21:29 +0000
Subject: [PATCH 5/6] Applies clang-format to the addedfiles

---
 regression/contracts/function-calls-01/main.c   |  3 +--
 regression/contracts/function-calls-02-1/main.c | 10 ++++------
 regression/contracts/function-calls-02/main.c   | 10 ++++------
 regression/contracts/function-calls-03-1/main.c | 11 +++++------
 regression/contracts/function-calls-03/main.c   | 11 +++++------
 regression/contracts/function-calls-04-1/main.c | 16 +++++++---------
 regression/contracts/function-calls-04/main.c   | 16 +++++++---------
 7 files changed, 33 insertions(+), 44 deletions(-)

diff --git a/regression/contracts/function-calls-01/main.c b/regression/contracts/function-calls-01/main.c
index 09ca17fc558..26f8445d361 100644
--- a/regression/contracts/function-calls-01/main.c
+++ b/regression/contracts/function-calls-01/main.c
@@ -1,5 +1,4 @@
-int f1(int *x1)
-  __CPROVER_requires(*x1 > 1 && *x1 < 10000)
+int f1(int *x1) __CPROVER_requires(*x1 > 1 && *x1 < 10000)
   __CPROVER_ensures(__CPROVER_return_value == *x1 + 1)
 {
   return *x1 + 1;
diff --git a/regression/contracts/function-calls-02-1/main.c b/regression/contracts/function-calls-02-1/main.c
index a6aeae94a8e..43a06e3ef3b 100644
--- a/regression/contracts/function-calls-02-1/main.c
+++ b/regression/contracts/function-calls-02-1/main.c
@@ -1,21 +1,19 @@
-int f1(int *x1)
-  __CPROVER_requires(*x1 > 1 && *x1 < 10000)
+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)
+int f2(int *x2) __CPROVER_requires(*x2 > 2 && *x2 < 10001)
   __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
 {
-  return *x2 + 1 ;
+  return *x2 + 1;
 }
 
 int main()
 {
-  int p; 
+  int p;
   __CPROVER_assume(p > 1 && p < 10000);
   f1(&p);
 
diff --git a/regression/contracts/function-calls-02/main.c b/regression/contracts/function-calls-02/main.c
index 560695c0856..9c698ec912d 100644
--- a/regression/contracts/function-calls-02/main.c
+++ b/regression/contracts/function-calls-02/main.c
@@ -1,20 +1,18 @@
-int f1(int *x1)
-  __CPROVER_requires(*x1 > 1 && *x1 < 10000)
+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)
+int f2(int *x2) __CPROVER_requires(*x2 > 1 && *x2 < 10000)
   __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
 {
-  return *x2 + 1 ;
+  return *x2 + 1;
 }
 
 int main()
 {
-  int p; 
+  int p;
   __CPROVER_assume(p > 1 && p < 10000);
   f1(&p);
 
diff --git a/regression/contracts/function-calls-03-1/main.c b/regression/contracts/function-calls-03-1/main.c
index f0df8a62097..ed53e1e5d31 100644
--- a/regression/contracts/function-calls-03-1/main.c
+++ b/regression/contracts/function-calls-03-1/main.c
@@ -1,22 +1,21 @@
-int f1(int *x1)
-  __CPROVER_requires(*x1 > 0 && *x1 < 20)
+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)
+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
+  if(*x2 < 1)
+    return -1; //Notice the change for the base case
   int loc = *x2 - 1;
   return f2(&loc) + 1;
 }
 
 int main()
 {
-  int p ; 
+  int p;
   __CPROVER_assume(p > 0 && p < 20);
   f1(&p);
 
diff --git a/regression/contracts/function-calls-03/main.c b/regression/contracts/function-calls-03/main.c
index 4f466a3b891..203ffd82a70 100644
--- a/regression/contracts/function-calls-03/main.c
+++ b/regression/contracts/function-calls-03/main.c
@@ -1,22 +1,21 @@
-int f1(int *x1)
-  __CPROVER_requires(*x1 > 0 && *x1 < 20)
+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)
+int f2(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
   __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
 {
-  if (*x2 < 1) return 1;
+  if(*x2 < 1)
+    return 1;
   int loc = *x2 - 1;
   return f2(&loc) + 1;
 }
 
 int main()
 {
-  int p ; 
+  int p;
   __CPROVER_assume(p > 0 && p < 20);
   f1(&p);
 
diff --git a/regression/contracts/function-calls-04-1/main.c b/regression/contracts/function-calls-04-1/main.c
index a5b160f3f87..36136e08bd2 100644
--- a/regression/contracts/function-calls-04-1/main.c
+++ b/regression/contracts/function-calls-04-1/main.c
@@ -1,21 +1,19 @@
-int f1(int *x1)
-  __CPROVER_requires(*x1 > 0 && *x1 < 20)
+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)
+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;
+  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)
+int f2_in(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 19)
   __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
 {
   return f2_out(x2);
@@ -23,7 +21,7 @@ int f2_in(int *x2)
 
 int main()
 {
-  int p ; 
+  int p;
   __CPROVER_assume(p > 0 && p < 20);
   f1(&p);
 
diff --git a/regression/contracts/function-calls-04/main.c b/regression/contracts/function-calls-04/main.c
index d9876b4e89c..f3aced38c72 100644
--- a/regression/contracts/function-calls-04/main.c
+++ b/regression/contracts/function-calls-04/main.c
@@ -1,21 +1,19 @@
-int f1(int *x1)
-  __CPROVER_requires(*x1 > 0 && *x1 < 20)
+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)
+int f2_out(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 20)
   __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
 {
-  if (*x2 < 1) return 1;
-  int loc2 = *x2-1;
+  if(*x2 < 1)
+    return 1;
+  int loc2 = *x2 - 1;
   return f2_in(&loc2) + 1;
 }
 
-int f2_in(int *x2)
-  __CPROVER_requires(*x2 >= 0 && *x2 < 19)
+int f2_in(int *x2) __CPROVER_requires(*x2 >= 0 && *x2 < 19)
   __CPROVER_ensures(__CPROVER_return_value == *x2 + 1)
 {
   return f2_out(x2);
@@ -23,7 +21,7 @@ int f2_in(int *x2)
 
 int main()
 {
-  int p ; 
+  int p;
   __CPROVER_assume(p > 0 && p < 20);
   f1(&p);
 

From 01444b7eeef30ebfa85004ebeb0d35f3e85f9fa2 Mon Sep 17 00:00:00 2001
From: Aren Babikian
 <babikian@dev-dsk-babikian-1d-e8327e0f.us-east-1.amazon.com>
Date: Thu, 11 Mar 2021 18:43:21 +0000
Subject: [PATCH 6/6] Assesses PR comments and adds handling for loop unwinding

---
 regression/contracts/chain.sh                     | 14 +++++++++++---
 .../contracts/function-calls-01/test-enf.desc     |  5 ++++-
 .../contracts/function-calls-01/test-rep.desc     |  5 ++++-
 .../contracts/function-calls-02-1/test-enf.desc   |  7 +++++--
 .../contracts/function-calls-02-1/test-mix.desc   |  6 +++++-
 .../contracts/function-calls-02-1/test-rep.desc   |  8 +++++++-
 .../contracts/function-calls-02/test-enf.desc     |  7 +++++--
 .../contracts/function-calls-02/test-mix.desc     |  6 +++++-
 .../contracts/function-calls-02/test-rep.desc     |  8 +++++++-
 .../contracts/function-calls-03-1/test-enf.desc   | 13 +++++++------
 .../contracts/function-calls-03/test-enf.desc     | 14 +++++++-------
 .../contracts/function-calls-03/test-mix.desc     |  6 +++++-
 .../contracts/function-calls-03/test-rep.desc     |  8 +++++++-
 .../contracts/function-calls-04-1/test-enf.desc   | 14 ++++++++------
 .../contracts/function-calls-04/test-enf.desc     | 15 ++++++++-------
 .../contracts/function-calls-04/test-mix-1.desc   |  9 ++++++++-
 .../contracts/function-calls-04/test-mix-2.desc   |  8 ++++++--
 .../contracts/function-calls-04/test-rep.desc     |  9 ++++++++-
 18 files changed, 117 insertions(+), 45 deletions(-)

diff --git a/regression/contracts/chain.sh b/regression/contracts/chain.sh
index a22dc195bdc..b79aae965bb 100755
--- a/regression/contracts/chain.sh
+++ b/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}
diff --git a/regression/contracts/function-calls-01/test-enf.desc b/regression/contracts/function-calls-01/test-enf.desc
index b2d6674d02a..1b660f56d87 100644
--- a/regression/contracts/function-calls-01/test-enf.desc
+++ b/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
diff --git a/regression/contracts/function-calls-01/test-rep.desc b/regression/contracts/function-calls-01/test-rep.desc
index 4775f50bbb6..d28bfcfb20b 100644
--- a/regression/contracts/function-calls-01/test-rep.desc
+++ b/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
diff --git a/regression/contracts/function-calls-02-1/test-enf.desc b/regression/contracts/function-calls-02-1/test-enf.desc
index 589e5fcce21..817b7b9c8d8 100644
--- a/regression/contracts/function-calls-02-1/test-enf.desc
+++ b/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.
diff --git a/regression/contracts/function-calls-02-1/test-mix.desc b/regression/contracts/function-calls-02-1/test-mix.desc
index f0c8b6818c0..edd25ca30be 100644
--- a/regression/contracts/function-calls-02-1/test-mix.desc
+++ b/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
diff --git a/regression/contracts/function-calls-02-1/test-rep.desc b/regression/contracts/function-calls-02-1/test-rep.desc
index c3b2440cb07..707cdf87fc8 100644
--- a/regression/contracts/function-calls-02-1/test-rep.desc
+++ b/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.
diff --git a/regression/contracts/function-calls-02/test-enf.desc b/regression/contracts/function-calls-02/test-enf.desc
index 589e5fcce21..817b7b9c8d8 100644
--- a/regression/contracts/function-calls-02/test-enf.desc
+++ b/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.
diff --git a/regression/contracts/function-calls-02/test-mix.desc b/regression/contracts/function-calls-02/test-mix.desc
index f0c8b6818c0..edd25ca30be 100644
--- a/regression/contracts/function-calls-02/test-mix.desc
+++ b/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
diff --git a/regression/contracts/function-calls-02/test-rep.desc b/regression/contracts/function-calls-02/test-rep.desc
index c3b2440cb07..707cdf87fc8 100644
--- a/regression/contracts/function-calls-02/test-rep.desc
+++ b/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.
diff --git a/regression/contracts/function-calls-03-1/test-enf.desc b/regression/contracts/function-calls-03-1/test-enf.desc
index ec16ceefc94..859a593e234 100644
--- a/regression/contracts/function-calls-03-1/test-enf.desc
+++ b/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.
diff --git a/regression/contracts/function-calls-03/test-enf.desc b/regression/contracts/function-calls-03/test-enf.desc
index 0ee5122b46b..fdbd93aacd0 100644
--- a/regression/contracts/function-calls-03/test-enf.desc
+++ b/regression/contracts/function-calls-03/test-enf.desc
@@ -1,19 +1,19 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^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
 
 Recursion:
 The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
 
-Known bug 1:
+Known bug:
 Enforce flag not handled correctly for function calls within functions.
-This bug is fixed in PR #5538.
-
-Known bug 2:
-This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.
diff --git a/regression/contracts/function-calls-03/test-mix.desc b/regression/contracts/function-calls-03/test-mix.desc
index 06afa685d2a..ffc11785616 100644
--- a/regression/contracts/function-calls-03/test-mix.desc
+++ b/regression/contracts/function-calls-03/test-mix.desc
@@ -6,7 +6,11 @@ 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
 
 Recursion:
 The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
diff --git a/regression/contracts/function-calls-03/test-rep.desc b/regression/contracts/function-calls-03/test-rep.desc
index 6c3eba4ffbe..cca10ac941f 100644
--- a/regression/contracts/function-calls-03/test-rep.desc
+++ b/regression/contracts/function-calls-03/test-rep.desc
@@ -6,7 +6,13 @@ 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.
 
 Recursion:
 The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions).
diff --git a/regression/contracts/function-calls-04-1/test-enf.desc b/regression/contracts/function-calls-04-1/test-enf.desc
index 4a3da990e58..4ca0e5e7948 100644
--- a/regression/contracts/function-calls-04-1/test-enf.desc
+++ b/regression/contracts/function-calls-04-1/test-enf.desc
@@ -1,18 +1,20 @@
-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 f1, f2_out and f2_in.
+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).
-
-Known bug:
-This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.
diff --git a/regression/contracts/function-calls-04/test-enf.desc b/regression/contracts/function-calls-04/test-enf.desc
index 1969af0f946..808cdab1356 100644
--- a/regression/contracts/function-calls-04/test-enf.desc
+++ b/regression/contracts/function-calls-04/test-enf.desc
@@ -1,19 +1,20 @@
 KNOWNBUG
 main.c
---enforce-all-contracts
+--enforce-all-contracts _ --unwind 20 --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the postconditions of f1, f2_out and f2_in.
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2_out   | assumed  | asserted
+  f2_in    | 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 1:
+Known bug:
 Enforce flag not handled correctly for function calls within functions.
-This bug is fixed in PR #5538.
-
-Known bug 2:
-This test requires the "--unwind 20 --unwinding-assertions" flag for the cbmc call in "chain.sh", which is currently not handled.
diff --git a/regression/contracts/function-calls-04/test-mix-1.desc b/regression/contracts/function-calls-04/test-mix-1.desc
index c7e87562c3c..3073097c3ee 100644
--- a/regression/contracts/function-calls-04/test-mix-1.desc
+++ b/regression/contracts/function-calls-04/test-mix-1.desc
@@ -6,7 +6,14 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the preconditions of f2_out (called from f1) and of the postconditions of f1.
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2_out   | asserted | assumed
+  f2_in    | n/a      | n/a
+
+Note: the calls to f2_in does not occur because the call to f2_out 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).
diff --git a/regression/contracts/function-calls-04/test-mix-2.desc b/regression/contracts/function-calls-04/test-mix-2.desc
index 01430c7905e..243d70b6f19 100644
--- a/regression/contracts/function-calls-04/test-mix-2.desc
+++ b/regression/contracts/function-calls-04/test-mix-2.desc
@@ -6,7 +6,12 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This confirms the accuracy of the preconditions of f2_in (called from f2_out) and of the postconditions of f1 and of f2_out.
+Verification:
+  function | pre-cond | post-cond
+  ---------|----------|----------
+  f1       | assumed  | asserted
+  f2_out   | assumed  | asserted
+  f2_in    | asserted | assumed
 
 Recursion
 (1) This test checks the mutualy recursive f2_out and f2-in functions by enforcing f2_out and replacing the internal f2_in call with its contract.
@@ -15,4 +20,3 @@ Recursion
 
 Known bug:
 Enforce flag not handled correctly for function calls within functions.
-This bug is fixed in PR #5538.
diff --git a/regression/contracts/function-calls-04/test-rep.desc b/regression/contracts/function-calls-04/test-rep.desc
index 6c3eba4ffbe..0551bd1a6b7 100644
--- a/regression/contracts/function-calls-04/test-rep.desc
+++ b/regression/contracts/function-calls-04/test-rep.desc
@@ -6,7 +6,14 @@ 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_out   | n/a      | n/a
+  f2_in    | n/a      | n/a
+
+Note: the calls to f2_out and to f2_in do 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).