Supports quantifiers in function contracts

regression/contracts/function_check_02/test.desc

@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---check-code-contracts
+--enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/quantifiers-exists-both-01/main.c

@@ -0,0 +1,18 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 8) ==> arr[i] == 0
+}) __CPROVER_ensures(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 8) ==> arr[i] == 0
+})
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[8];
+  f1(arr);
+}

regression/contracts/quantifiers-exists-both-01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+in a negative context (which is currently not always the case). By using the
+--enforce-all-contracts flag, this test assumes the statement in 
+__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures),
+thus, verification should be successful.

regression/contracts/quantifiers-exists-both-02/main.c

@@ -0,0 +1,18 @@
+// clang-format off
+int f1(int *arr, int *len) __CPROVER_requires(__CPROVER_exists {
+  int i;
+  (0 <= i && i < len) ==> arr[i] == 0
+}) __CPROVER_ensures(__CPROVER_exists {
+  int i;
+  (0 <= i && i < len) ==> arr[i] == 0
+})
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int len, arr[8];
+  f1(arr, len);
+}

regression/contracts/quantifiers-exists-both-02/test.desc

@@ -0,0 +1,19 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+in a negative context (which is currently not always the case). By using the
+--enforce-all-contracts flag, this test assumes the statement in 
+__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures),
+thus, verification should be successful.
+
+Known bug:
+The current implementation cannot handle a structure such as
+__CPROVER_assume(__CPROVER_exists(int i; pred(i))), where i is
+not explicitly bounded to a predefined range (i.e. if at least
+one of its bound is only declared and not defined).

regression/contracts/quantifiers-exists-ensures-01/main.c

@@ -0,0 +1,20 @@
+// clang-format off
+int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == i
+})
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = i;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr);
+}

regression/contracts/quantifiers-exists-ensures-01/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag, 
+goto-instrument will transform the __CPROVER_ensures clauses into an
+assertion and the verification remains sound when using __CPROVER_exists.

regression/contracts/quantifiers-exists-ensures-02/main.c

@@ -0,0 +1,20 @@
+// clang-format off
+int f1(int *arr) __CPROVER_ensures(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] != 0
+})
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = 0;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr);
+}

regression/contracts/quantifiers-exists-ensures-02/test.desc

@@ -0,0 +1,19 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag, 
+goto-instrument will transform the __CPROVER_ensures clauses into an
+assertion and the verification remains sound when using __CPROVER_exists.
+
+Known Bug:
+We expect verification to fail because arr[i] is always equal to 0 for
+[0 <= i < 10]. In fact, we expect the (0 <= i && i < 10) statement to act as a
+range for i. However, in the current implementation of quantifier handling,
+the (0 <= i && i < 10) statement is not interpreted as an explicit range, but
+instead, as part of a logic formula, which causes verification to succeed.

regression/contracts/quantifiers-exists-requires-01/main.c

@@ -0,0 +1,15 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == 4
+}) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+  f1(arr);
+}

regression/contracts/quantifiers-exists-requires-01/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
+flag, goto-instrument will transform the __CPROVER_requires clauses into an
+assertion and the verification remains sound when using __CPROVER_exists.

regression/contracts/quantifiers-exists-requires-02/main.c

@@ -0,0 +1,15 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(__CPROVER_exists {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == 1
+}) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
+  f1(arr);
+}

regression/contracts/quantifiers-exists-requires-02/test.desc

@@ -0,0 +1,19 @@
+KNOWNBUG
+main.c
+--replace-all-calls-with-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_exists
+in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
+flag, goto-instrument will transform the __CPROVER_requires clauses into an
+assertion and the verification remains sound when using __CPROVER_exists.
+
+Known Bug:
+We expect verification to fail because arr[i] is never equal to 1 for
+[0 <= i < 10]. In fact, we expect the (0 <= i && i < 10) statement to act as a
+range for i. However, in the current implementation of quantifier handling,
+the (0 <= i && i < 10) statement is not interpreted as an explicit range, but
+instead, as part of a logic formula, which causes verification to succeed.

regression/contracts/quantifiers-forall-both-01/main.c

@@ -0,0 +1,18 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
+  int i;
+  (0 <= i && i < 8) ==> arr[i] == 0
+}) __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  (0 <= i && i < 8) ==> arr[i] == 0
+})
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[8];
+  f1(arr);
+}

regression/contracts/quantifiers-forall-both-01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall
+in a negative context (which is currently not always the case). By using the
+--enforce-all-contracts flag, this test assumes the statement in
+__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures), 
+thus, verification should be successful.

regression/contracts/quantifiers-forall-both-02/main.c

@@ -0,0 +1,18 @@
+// clang-format off
+int f1(int *arr, int len) __CPROVER_requires(__CPROVER_forall {
+  int i;
+  (0 <= i && i < len) ==> arr[i] == 0
+}) __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  (0 <= i && i < len) ==> arr[i] == 0
+})
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int len, arr[8];
+  f1(arr, len);
+}

regression/contracts/quantifiers-forall-both-02/test.desc

@@ -0,0 +1,19 @@
+KNOWNBUG
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall
+in a negative context (which is currently not always the case). By using the
+--enforce-all-contracts flag, this test assumes the statement in
+__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures), 
+thus, verification should be successful.
+
+Known bug:
+The current implementation cannot handle a structure such as
+__CPROVER_assume(__CPROVER_forall(int i; pred(i))), where i is
+not explicitly bounded to a predefined range (i.e. if at least
+one of its bound is only declared and not defined).

regression/contracts/quantifiers-forall-ensures-01/main.c

@@ -0,0 +1,20 @@
+// clang-format off
+int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == 0
+})
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    arr[i] = 0;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr);
+}

regression/contracts/quantifiers-forall-ensures-01/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall
+in __CPROVER_ensures clauses. By using the --enforce-all-contracts
+flag, goto-instrument will transform the __CPROVER_ensures clauses into an
+assertion and the verification remains sound when using __CPROVER_forall.

regression/contracts/quantifiers-forall-ensures-02/main.c

@@ -0,0 +1,23 @@
+// clang-format off
+int f1(int *arr) __CPROVER_ensures(__CPROVER_forall {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == i
+})
+// clang-format on
+{
+  for(int i = 0; i < 10; i++)
+  {
+    if(i == 0)
+      arr[i] = -1;
+    else
+      arr[i] = i;
+  }
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  f1(arr);
+}

regression/contracts/quantifiers-forall-ensures-02/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall
+in __CPROVER_ensures clauses. By using the --enforce-all-contracts
+flag, goto-instrument will transform the __CPROVER_ensures clauses into an
+assertion and the verification remains sound when using __CPROVER_forall.

regression/contracts/quantifiers-forall-requires-01/main.c

@@ -0,0 +1,15 @@
+// clang-format off
+int f1(int *arr) __CPROVER_requires(__CPROVER_forall {
+  int i;
+  (0 <= i && i < 10) ==> arr[i] == i
+}) __CPROVER_ensures(__CPROVER_return_value == 0)
+// clang-format on
+{
+  return 0;
+}
+
+int main()
+{
+  int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9};
+  f1(arr);
+}

regression/contracts/quantifiers-forall-requires-01/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--replace-all-calls-with-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+The purpose of this test is to ensure that we can safely use __CPROVER_forall
+in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts
+flag, goto-instrument will transform the __CPROVER_requires clauses into an
+assertion and the verification remains sound when using __CPROVER_forall.