From 56e0b20dba4f439d119bb8c38e183403b25c7013 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Mon, 24 May 2021 16:36:52 -0400 Subject: [PATCH 1/2] Cleanup regression tests for quantified contracts --- .../quantifiers-exists-both-01/main.c | 16 ++++--- .../quantifiers-exists-both-01/test.desc | 13 +++--- .../quantifiers-exists-both-02/main.c | 40 +++++++++++++---- .../quantifiers-exists-both-02/test.desc | 21 ++++----- .../quantifiers-exists-ensures-01/main.c | 20 ++++++++- .../quantifiers-exists-ensures-01/test.desc | 13 +++--- .../quantifiers-exists-ensures-02/main.c | 43 ++++++++++++++----- .../quantifiers-exists-ensures-02/test.desc | 19 +++----- .../quantifiers-exists-requires-01/main.c | 38 +++++++++++++--- .../quantifiers-exists-requires-01/test.desc | 10 +++-- .../quantifiers-exists-requires-02/main.c | 27 ++++++++++-- .../quantifiers-exists-requires-02/test.desc | 18 ++++---- .../quantifiers-forall-both-01/main.c | 16 ++++--- .../quantifiers-forall-both-01/test.desc | 13 +++--- .../quantifiers-forall-both-02/main.c | 36 ++++++++++++---- .../quantifiers-forall-both-02/test.desc | 21 ++++----- .../quantifiers-forall-ensures-01/main.c | 22 +++++++--- .../quantifiers-forall-ensures-01/test.desc | 8 ++-- .../quantifiers-forall-ensures-02/main.c | 31 +++++++------ .../quantifiers-forall-ensures-02/test.desc | 12 ++++-- .../quantifiers-forall-requires-01/main.c | 21 ++++++--- .../quantifiers-forall-requires-01/test.desc | 12 ++++-- .../quantifiers-forall-requires-02/main.c | 30 ++++++++++--- .../quantifiers-forall-requires-02/test.desc | 12 +++--- .../contracts/quantifiers-loop-01/test.desc | 1 + .../contracts/quantifiers-loop-02/test.desc | 15 ++++--- .../contracts/quantifiers-loop-03/test.desc | 1 + .../contracts/quantifiers-nested-01/test.desc | 2 +- .../contracts/quantifiers-nested-02/main.c | 20 +++++---- .../contracts/quantifiers-nested-02/test.desc | 2 +- .../contracts/quantifiers-nested-03/main.c | 16 ++++--- .../contracts/quantifiers-nested-03/test.desc | 2 +- .../contracts/quantifiers-nested-04/main.c | 25 ++++++----- .../contracts/quantifiers-nested-04/test.desc | 2 +- .../contracts/quantifiers-nested-05/main.c | 14 ++++-- .../contracts/quantifiers-nested-05/test.desc | 2 +- .../contracts/quantifiers-nested-06/main.c | 39 +++++++++++------ .../contracts/quantifiers-nested-06/test.desc | 2 +- 38 files changed, 436 insertions(+), 219 deletions(-) diff --git a/regression/contracts/quantifiers-exists-both-01/main.c b/regression/contracts/quantifiers-exists-both-01/main.c index c123d0c837d..d245284d067 100644 --- a/regression/contracts/quantifiers-exists-both-01/main.c +++ b/regression/contracts/quantifiers-exists-both-01/main.c @@ -1,11 +1,13 @@ // 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 -}) +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; diff --git a/regression/contracts/quantifiers-exists-both-01/test.desc b/regression/contracts/quantifiers-exists-both-01/test.desc index ee6c03641c5..433b9abb6a1 100644 --- a/regression/contracts/quantifiers-exists-both-01/test.desc +++ b/regression/contracts/quantifiers-exists-both-01/test.desc @@ -3,11 +3,14 @@ main.c --enforce-all-contracts ^EXIT=0$ ^SIGNAL=0$ +^\[1\] assertion: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -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. +The purpose of this test is to ensure that we can safely use __CPROVER_exists within both +positive and negative contexts (ENSURES and REQUIRES clauses). + +With the SAT backend existential quantifiers in a positive context, +e.g., the ENSURES clause being enforced in this case, +are supported only if the quantifier is bound to a constant range. diff --git a/regression/contracts/quantifiers-exists-both-02/main.c b/regression/contracts/quantifiers-exists-both-02/main.c index d5a5655bb3d..85360a7f075 100644 --- a/regression/contracts/quantifiers-exists-both-02/main.c +++ b/regression/contracts/quantifiers-exists-both-02/main.c @@ -1,11 +1,29 @@ +#include + +#define MAX_LEN 8 + // 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 -}) +int f1(int *arr, int len) + __CPROVER_requires( + len > 0 ==> __CPROVER_exists { + int i; + // constant bounds for explicit unrolling with SAT backend + (0 <= i && i < MAX_LEN) && ( + // actual symbolic bound for `i` + i < len && arr[i] == 0 + ) + } + ) + __CPROVER_ensures( + len > 0 ==> __CPROVER_exists { + int i; + // constant bounds for explicit unrolling with SAT backend + (0 <= i && i < MAX_LEN) && ( + // actual symbolic bound for `i` + i < len && arr[i] == 0 + ) + } + ) // clang-format on { return 0; @@ -13,6 +31,12 @@ int f1(int *arr, int *len) __CPROVER_requires(__CPROVER_exists { int main() { - int len, arr[8]; + int len; + __CPROVER_assume(0 <= len && len <= MAX_LEN); + + int *arr = malloc(len); + if(len > 0) + arr[0] = 0; + f1(arr, len); } diff --git a/regression/contracts/quantifiers-exists-both-02/test.desc b/regression/contracts/quantifiers-exists-both-02/test.desc index a8ecf5ff952..2bafb11eaf0 100644 --- a/regression/contracts/quantifiers-exists-both-02/test.desc +++ b/regression/contracts/quantifiers-exists-both-02/test.desc @@ -1,19 +1,16 @@ -KNOWNBUG +CORE main.c ---enforce-all-contracts +--replace-all-calls-with-contracts ^EXIT=0$ ^SIGNAL=0$ +^\[1\] assertion: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -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. +The purpose of this test is to ensure that we can safely use __CPROVER_exists within both +positive and negative contexts (ENSURES and REQUIRES clauses). -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). +With the SAT backend existential quantifiers in a positive context, +e.g., the REQUIRES clause being replaced in this case, +are supported only if the quantifier is bound to a constant range. diff --git a/regression/contracts/quantifiers-exists-ensures-01/main.c b/regression/contracts/quantifiers-exists-ensures-01/main.c index ad4d3964ed3..1194c2968de 100644 --- a/regression/contracts/quantifiers-exists-ensures-01/main.c +++ b/regression/contracts/quantifiers-exists-ensures-01/main.c @@ -3,7 +3,7 @@ int f1(int *arr) __CPROVER_assigns(*arr) __CPROVER_ensures(__CPROVER_exists { int i; - (0 <= i && i < 10) ==> arr[i] == i + (0 <= i && i < 10) && arr[i] == i }) // clang-format on { @@ -15,8 +15,26 @@ int f1(int *arr) return 0; } +// clang-format off +int f2(int *arr) + __CPROVER_assigns(*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]; + f2(arr); f1(arr); } diff --git a/regression/contracts/quantifiers-exists-ensures-01/test.desc b/regression/contracts/quantifiers-exists-ensures-01/test.desc index f1d037caa5f..dfe6e1ae24c 100644 --- a/regression/contracts/quantifiers-exists-ensures-01/test.desc +++ b/regression/contracts/quantifiers-exists-ensures-01/test.desc @@ -1,12 +1,15 @@ CORE main.c --enforce-all-contracts -^EXIT=0$ +^EXIT=10$ ^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ -- +^warning: ignoring -- 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. +within positive contexts (enforced ENSURES clauses). + +With the SAT backend existential quantifiers in a positive context, +e.g., the ENSURES clause being enforced in this case, +are supported only if the quantifier is bound to a constant range. diff --git a/regression/contracts/quantifiers-exists-ensures-02/main.c b/regression/contracts/quantifiers-exists-ensures-02/main.c index ea2a2fa88ac..caacb3e5ccb 100644 --- a/regression/contracts/quantifiers-exists-ensures-02/main.c +++ b/regression/contracts/quantifiers-exists-ensures-02/main.c @@ -1,20 +1,41 @@ +#include +#include +#include + +#define MAX_LEN 128 + // clang-format off -int f1(int *arr) __CPROVER_ensures(__CPROVER_exists { - int i; - (0 <= i && i < 10) ==> arr[i] != 0 -}) +int f1(int *arr, int len) + __CPROVER_ensures( + len > 0 ==> __CPROVER_exists { + int i; + // test replacement with symbolic bound + (0 <= i && i < len) && arr[i] == 0 + } + ) // clang-format on { - for(int i = 0; i < 10; i++) - { - arr[i] = 0; - } - + // we are only checking for contract replacement return 0; } int main() { - int arr[10]; - f1(arr); + int len; + __CPROVER_assume(0 <= len && len <= MAX_LEN); + + int *arr = malloc(len * sizeof(int)); + + f1(arr, len); + + bool found_zero = false; + for(int i = 0; i <= MAX_LEN; i++) + { + if(i < len) + found_zero |= (arr[i] == 0); + } + + // clang-format off + assert(len > 0 ==> found_zero); + // clang-format on } diff --git a/regression/contracts/quantifiers-exists-ensures-02/test.desc b/regression/contracts/quantifiers-exists-ensures-02/test.desc index 473f8e20622..09144241702 100644 --- a/regression/contracts/quantifiers-exists-ensures-02/test.desc +++ b/regression/contracts/quantifiers-exists-ensures-02/test.desc @@ -1,19 +1,14 @@ CORE main.c ---enforce-all-contracts -^EXIT=10$ +--replace-all-calls-with-contracts +^EXIT=0$ ^SIGNAL=0$ -^VERIFICATION FAILED$ +^\[main.assertion.1\] line .* assertion len > 0 ==> found_zero: SUCCESS$ +^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- 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. +within negative contexts (replaced ENSURES clauses). -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. +This is fully supported (without requiring full unrolling) with the SAT backend. diff --git a/regression/contracts/quantifiers-exists-requires-01/main.c b/regression/contracts/quantifiers-exists-requires-01/main.c index aefde2c93bc..7985f57de3b 100644 --- a/regression/contracts/quantifiers-exists-requires-01/main.c +++ b/regression/contracts/quantifiers-exists-requires-01/main.c @@ -1,15 +1,39 @@ +#include +#include + +#define MAX_LEN 64 + // 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) +bool f1(int *arr, int len) + __CPROVER_requires( + len > 0 ==> __CPROVER_exists { + int i; + // test enforcement with symbolic bound + (0 <= i && i < len) && arr[i] == 4 + } + ) + __CPROVER_ensures( + __CPROVER_return_value == true + ) // clang-format on { - return 0; + bool found_four = false; + for(int i = 0; i <= MAX_LEN; i++) + { + if(i < len) + found_four |= (arr[i] == 4); + } + + // clang-format off + return (len > 0 ==> found_four); + // clang-format on } int main() { - int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; - f1(arr); + int len; + __CPROVER_assume(0 <= len && len <= MAX_LEN); + + int *arr = malloc(len * sizeof(int)); + f1(arr, len); } diff --git a/regression/contracts/quantifiers-exists-requires-01/test.desc b/regression/contracts/quantifiers-exists-requires-01/test.desc index 60d164515f5..898df96cf06 100644 --- a/regression/contracts/quantifiers-exists-requires-01/test.desc +++ b/regression/contracts/quantifiers-exists-requires-01/test.desc @@ -1,12 +1,14 @@ CORE main.c ---replace-all-calls-with-contracts +--enforce-all-contracts ^EXIT=0$ ^SIGNAL=0$ +^\[1\] assertion: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- 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. +within both negative contexts (enforced REQUIRES clauses). + +This is fully supported (without requiring full unrolling) with the SAT backend. diff --git a/regression/contracts/quantifiers-exists-requires-02/main.c b/regression/contracts/quantifiers-exists-requires-02/main.c index db36c3c41c9..f7c1e5f896a 100644 --- a/regression/contracts/quantifiers-exists-requires-02/main.c +++ b/regression/contracts/quantifiers-exists-requires-02/main.c @@ -1,8 +1,26 @@ // 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) +int f1(int *arr) + __CPROVER_requires(__CPROVER_exists { + int i; + (0 <= i && i < 10) && arr[i] == 0 + }) + __CPROVER_ensures( + __CPROVER_return_value == 0 + ) +// clang-format on +{ + return 0; +} + +// clang-format off +int f2(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; @@ -12,4 +30,5 @@ int main() { int arr[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0}; f1(arr); + f2(arr); } diff --git a/regression/contracts/quantifiers-exists-requires-02/test.desc b/regression/contracts/quantifiers-exists-requires-02/test.desc index f00b0c7fdb2..9d310e67dd7 100644 --- a/regression/contracts/quantifiers-exists-requires-02/test.desc +++ b/regression/contracts/quantifiers-exists-requires-02/test.desc @@ -1,19 +1,17 @@ -KNOWNBUG +CORE main.c --replace-all-calls-with-contracts ^EXIT=10$ ^SIGNAL=0$ +^\[1\] assertion: SUCCESS$ +^\[2\] assertion: FAILURE$ ^VERIFICATION FAILED$ -- +^warning: ignoring -- 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. +within both positive contexts (replaced REQUIRES clauses). -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. +With the SAT backend existential quantifiers in a positive context, +e.g., the REQUIRES clause being replaced in this case, +are supported only if the quantifier is bound to a constant range. diff --git a/regression/contracts/quantifiers-forall-both-01/main.c b/regression/contracts/quantifiers-forall-both-01/main.c index a9533000171..d47d59bcc3e 100644 --- a/regression/contracts/quantifiers-forall-both-01/main.c +++ b/regression/contracts/quantifiers-forall-both-01/main.c @@ -1,11 +1,13 @@ // 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 -}) +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; diff --git a/regression/contracts/quantifiers-forall-both-01/test.desc b/regression/contracts/quantifiers-forall-both-01/test.desc index c7f16fc8c51..994099cac27 100644 --- a/regression/contracts/quantifiers-forall-both-01/test.desc +++ b/regression/contracts/quantifiers-forall-both-01/test.desc @@ -3,11 +3,14 @@ main.c --enforce-all-contracts ^EXIT=0$ ^SIGNAL=0$ +^\[1\] assertion: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -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. +The purpose of this test is to ensure that we can safely use __CPROVER_forall within both +positive and negative contexts (ENSURES and REQUIRES clauses). + +With the SAT backend universal quantifiers in a negative context, +e.g., the REQUIRES clause being enforced in this case, +are supported only if the quantifier is bound to a constant range. diff --git a/regression/contracts/quantifiers-forall-both-02/main.c b/regression/contracts/quantifiers-forall-both-02/main.c index d173dba1469..0bfda4af0e1 100644 --- a/regression/contracts/quantifiers-forall-both-02/main.c +++ b/regression/contracts/quantifiers-forall-both-02/main.c @@ -1,11 +1,22 @@ +#include + +#define MAX_LEN 8 + // 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 -}) +int f1(int *arr, int len) + __CPROVER_requires(__CPROVER_forall { + int i; + // constant bounds for explicit unrolling with SAT backend + (0 <= i && i < MAX_LEN) ==> ( + // actual symbolic bound for `i` + i < len ==> arr[i] == 0 + ) + }) + __CPROVER_ensures(__CPROVER_forall { + int i; + // positive context, so symbolic bounds are fine + (0 <= i && i < len) ==> arr[i] == 0 + }) // clang-format on { return 0; @@ -13,6 +24,15 @@ int f1(int *arr, int len) __CPROVER_requires(__CPROVER_forall { int main() { - int len, arr[8]; + int len; + __CPROVER_assume(0 <= len && len <= MAX_LEN); + + int *arr = malloc(len); + for(int i = 0; i < MAX_LEN; ++i) + { + if(i < len) + arr[i] = 0; + } + f1(arr, len); } diff --git a/regression/contracts/quantifiers-forall-both-02/test.desc b/regression/contracts/quantifiers-forall-both-02/test.desc index 8b2381cfb3f..6b1e25a914c 100644 --- a/regression/contracts/quantifiers-forall-both-02/test.desc +++ b/regression/contracts/quantifiers-forall-both-02/test.desc @@ -1,19 +1,16 @@ -KNOWNBUG +CORE main.c ---enforce-all-contracts +--replace-all-calls-with-contracts ^EXIT=0$ ^SIGNAL=0$ +^\[1\] assertion: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -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. +The purpose of this test is to ensure that we can safely use __CPROVER_forall within both +positive and negative contexts (ENSURES and REQUIRES clauses). -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). +With the SAT backend universal quantifiers in a negative context, +e.g., the ENSURES clause being replaced in this case, +are supported only if the quantifier is bound to a constant range. diff --git a/regression/contracts/quantifiers-forall-ensures-01/main.c b/regression/contracts/quantifiers-forall-ensures-01/main.c index 7e601ea0282..78271197aec 100644 --- a/regression/contracts/quantifiers-forall-ensures-01/main.c +++ b/regression/contracts/quantifiers-forall-ensures-01/main.c @@ -1,22 +1,30 @@ +#include + +#define MAX_LEN 16 + // clang-format off -int f1(int *arr) +int f1(int *arr, int len) __CPROVER_assigns(*arr) __CPROVER_ensures(__CPROVER_forall { int i; - (0 <= i && i < 10) ==> arr[i] == 0 + // test enforcement with symbolic bound + (0 <= i && i < len) ==> arr[i] == 0 }) // clang-format on { - for(int i = 0; i < 10; i++) + for(int i = 0; i < MAX_LEN; i++) { - arr[i] = 0; + if(i < len) + arr[i] = 0; } - return 0; } int main() { - int arr[10]; - f1(arr); + int len; + __CPROVER_assume(0 <= len && len <= MAX_LEN); + + int *arr = malloc(len * sizeof(int)); + f1(arr, len); } diff --git a/regression/contracts/quantifiers-forall-ensures-01/test.desc b/regression/contracts/quantifiers-forall-ensures-01/test.desc index 44769e5ca27..63cc32c4b1d 100644 --- a/regression/contracts/quantifiers-forall-ensures-01/test.desc +++ b/regression/contracts/quantifiers-forall-ensures-01/test.desc @@ -3,10 +3,12 @@ main.c --enforce-all-contracts ^EXIT=0$ ^SIGNAL=0$ +^\[1\] assertion: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- 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. +within positive contexts (enforced ENSURES clauses). + +This is fully supported (without requiring full unrolling) with the SAT backend. diff --git a/regression/contracts/quantifiers-forall-ensures-02/main.c b/regression/contracts/quantifiers-forall-ensures-02/main.c index 7904224f227..8a9da439097 100644 --- a/regression/contracts/quantifiers-forall-ensures-02/main.c +++ b/regression/contracts/quantifiers-forall-ensures-02/main.c @@ -1,23 +1,30 @@ +#include +#include + // clang-format off -int f1(int *arr) __CPROVER_ensures(__CPROVER_forall { - int i; - (0 <= i && i < 10) ==> arr[i] == i -}) +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); + + bool check = true; + for(int i = 0; i < 10; i++) + { + if(i == 0) + check &= (arr[i] = -1); + else + check &= (arr[i] = i); + } + assert(check); } diff --git a/regression/contracts/quantifiers-forall-ensures-02/test.desc b/regression/contracts/quantifiers-forall-ensures-02/test.desc index 3058ae57fd4..2fb1c6b035c 100644 --- a/regression/contracts/quantifiers-forall-ensures-02/test.desc +++ b/regression/contracts/quantifiers-forall-ensures-02/test.desc @@ -1,12 +1,16 @@ CORE main.c ---enforce-all-contracts +--replace-all-calls-with-contracts ^EXIT=10$ ^SIGNAL=0$ +^\[main.assertion.1\] line .* assertion check: FAILURE$ ^VERIFICATION FAILED$ -- +^warning: ignoring -- 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. +within negative contexts (replaced ENSURES clauses). + +With the SAT backend universal quantifiers within a negative context, +e.g., the ENSURES clause being replaced in this case, +are supported only if the quantifier is bound to a constant range. diff --git a/regression/contracts/quantifiers-forall-requires-01/main.c b/regression/contracts/quantifiers-forall-requires-01/main.c index 6470ce98056..fe0da19e0ca 100644 --- a/regression/contracts/quantifiers-forall-requires-01/main.c +++ b/regression/contracts/quantifiers-forall-requires-01/main.c @@ -1,15 +1,24 @@ +#include + // 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) +bool f1(int *arr) + __CPROVER_requires(__CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == i + }) + __CPROVER_ensures( + __CPROVER_return_value == true + ) // clang-format on { - return 0; + bool is_identity = true; + for(int i = 0; i < 10; ++i) + is_identity &= (arr[i] == i); + return is_identity; } int main() { - int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; + int arr[10]; f1(arr); } diff --git a/regression/contracts/quantifiers-forall-requires-01/test.desc b/regression/contracts/quantifiers-forall-requires-01/test.desc index cb5fe8567b9..143e769cc31 100644 --- a/regression/contracts/quantifiers-forall-requires-01/test.desc +++ b/regression/contracts/quantifiers-forall-requires-01/test.desc @@ -1,12 +1,16 @@ CORE main.c ---replace-all-calls-with-contracts +--enforce-all-contracts ^EXIT=0$ ^SIGNAL=0$ +^\[1\] assertion: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- 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. +within negative contexts (enforced REQUIRES clauses). + +With the SAT backend universal quantifiers within a negative context, +e.g., the REQUIRES clause being enforced in this case, +are supported only if the quantifier is bound to a constant range. diff --git a/regression/contracts/quantifiers-forall-requires-02/main.c b/regression/contracts/quantifiers-forall-requires-02/main.c index b8c4caab137..6c086f98719 100644 --- a/regression/contracts/quantifiers-forall-requires-02/main.c +++ b/regression/contracts/quantifiers-forall-requires-02/main.c @@ -1,8 +1,17 @@ +#include + +#define MAX_LEN 16 + // 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) +int f1(int *arr, int len) + __CPROVER_requires(__CPROVER_forall { + int i; + // test replacement with symbolic bound + (0 <= i && i < len) ==> arr[i] == i + }) + __CPROVER_ensures( + __CPROVER_return_value == 0 + ) // clang-format on { return 0; @@ -10,6 +19,15 @@ int f1(int *arr) __CPROVER_requires(__CPROVER_forall { int main() { - int arr[10] = {-1, 1, 2, 3, 4, 5, 6, 7, 8, 9}; - f1(arr); + int len; + __CPROVER_assume(0 <= len && len <= MAX_LEN); + + int *arr = malloc(len * sizeof(int)); + for(int i = 0; i < MAX_LEN; ++i) + { + if(i < len) + arr[i] = i; + } + + f1(arr, len); } diff --git a/regression/contracts/quantifiers-forall-requires-02/test.desc b/regression/contracts/quantifiers-forall-requires-02/test.desc index f841a39d8c8..63970dc4173 100644 --- a/regression/contracts/quantifiers-forall-requires-02/test.desc +++ b/regression/contracts/quantifiers-forall-requires-02/test.desc @@ -1,12 +1,14 @@ CORE main.c --replace-all-calls-with-contracts -^EXIT=10$ +^EXIT=0$ ^SIGNAL=0$ -^VERIFICATION FAILED$ +^\[1\] assertion: SUCCESS$ +^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- 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. +within positive contexts (replaced REQUIRES clauses). + +This is fully supported (without requiring full unrolling) with the SAT backend. \ No newline at end of file diff --git a/regression/contracts/quantifiers-loop-01/test.desc b/regression/contracts/quantifiers-loop-01/test.desc index b5f89638ead..be46c230b33 100644 --- a/regression/contracts/quantifiers-loop-01/test.desc +++ b/regression/contracts/quantifiers-loop-01/test.desc @@ -8,6 +8,7 @@ main.c ^\[main.assertion.1\] line .* assertion a\[10\] == 1: SUCCESS ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- This test case checks the handling of a `forall` quantifier within a loop invariant. diff --git a/regression/contracts/quantifiers-loop-02/test.desc b/regression/contracts/quantifiers-loop-02/test.desc index 7774449f536..d5367bac034 100644 --- a/regression/contracts/quantifiers-loop-02/test.desc +++ b/regression/contracts/quantifiers-loop-02/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG smt-backend broken-cprover-smt-backend +CORE main.c ---enforce-all-contracts +--enforce-all-contracts _ --z3 ^EXIT=0$ ^SIGNAL=0$ ^\[main.1\] line .* Check loop invariant before entry: SUCCESS @@ -8,14 +8,15 @@ main.c ^\[main.assertion.1\] line .* assertion .*: SUCCESS ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- This test case checks the handling of a universal quantifier, with a symbolic upper bound, within a loop invariant. -The test is tagged: -- `smt-backend`: +TODO: This test should: +- be tagged `smt-backend`: because the SAT backend does not support (simply ignores) `forall` in negative (e.g. assume) contexts. -- `broken-cprover-smt-backend`: +- be tagged `broken-cprover-smt-backend`: because the CPROVER SMT2 solver cannot handle (errors out on) `forall` in negative (e.g. assume) contexts. - -It has been tagged `KNOWNBUG` for now since `contracts` regression tests are not run with SMT backend yet. +- not use the `_ --z3` parameters: + once SMT-related tags are supported by the `Makefile`. diff --git a/regression/contracts/quantifiers-loop-03/test.desc b/regression/contracts/quantifiers-loop-03/test.desc index e728ab44d5b..429c07e0ec2 100644 --- a/regression/contracts/quantifiers-loop-03/test.desc +++ b/regression/contracts/quantifiers-loop-03/test.desc @@ -8,6 +8,7 @@ main.c ^\[main.assertion.1\] line .* assertion .*: SUCCESS ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- This test case checks the handling of an existential quantifier, with a symbolic upper bound, within a loop invariant. diff --git a/regression/contracts/quantifiers-nested-01/test.desc b/regression/contracts/quantifiers-nested-01/test.desc index 3a6b85c370b..cb7cecc36ae 100644 --- a/regression/contracts/quantifiers-nested-01/test.desc +++ b/regression/contracts/quantifiers-nested-01/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -Verification: This test case checks the handling of a forall expression nested within another forall expression. diff --git a/regression/contracts/quantifiers-nested-02/main.c b/regression/contracts/quantifiers-nested-02/main.c index 7cfa3051c01..0e43fb11d53 100644 --- a/regression/contracts/quantifiers-nested-02/main.c +++ b/regression/contracts/quantifiers-nested-02/main.c @@ -1,12 +1,16 @@ // clang-format off -int f1(int *arr) __CPROVER_requires(__CPROVER_forall { - int i; - 0 <= i && i < 9 ==> __CPROVER_forall - { - int j; - (i <= j && j < 10) ==> arr[i] <= arr[j] - } -}) __CPROVER_ensures(__CPROVER_return_value == 0) +int f1(int *arr) + __CPROVER_requires( + __CPROVER_forall { + int i; + (0 <= i && i < 9) ==> __CPROVER_forall { + int j; + (i <= j && j < 10) ==> arr[i] <= arr[j] + }} + ) + __CPROVER_ensures( + __CPROVER_return_value == 0 + ) // clang-format on { return 0; diff --git a/regression/contracts/quantifiers-nested-02/test.desc b/regression/contracts/quantifiers-nested-02/test.desc index 218e27b3671..0aaf256d1f9 100644 --- a/regression/contracts/quantifiers-nested-02/test.desc +++ b/regression/contracts/quantifiers-nested-02/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -Verification: This test case checks the handling of a forall expression nested within an implication. diff --git a/regression/contracts/quantifiers-nested-03/main.c b/regression/contracts/quantifiers-nested-03/main.c index eb991a2c8b2..ec26b365f81 100644 --- a/regression/contracts/quantifiers-nested-03/main.c +++ b/regression/contracts/quantifiers-nested-03/main.c @@ -1,8 +1,14 @@ -int f1(int *arr) __CPROVER_assigns(*arr) - __CPROVER_ensures(__CPROVER_return_value == 0 && __CPROVER_exists { - int i; - (0 <= i && i < 10) && arr[i] == i - }) +// clang-format off +int f1(int *arr) +__CPROVER_assigns(*arr) + __CPROVER_ensures( + __CPROVER_return_value == 0 && + __CPROVER_exists { + int i; + (0 <= i && i < 10) && arr[i] == i + } + ) +// clang-format on { for(int i = 0; i < 10; i++) { diff --git a/regression/contracts/quantifiers-nested-03/test.desc b/regression/contracts/quantifiers-nested-03/test.desc index ceeb1710f4b..4a811b6dcf8 100644 --- a/regression/contracts/quantifiers-nested-03/test.desc +++ b/regression/contracts/quantifiers-nested-03/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -Verification: This test case checks the handling of an exists expression nested within a conjunction. diff --git a/regression/contracts/quantifiers-nested-04/main.c b/regression/contracts/quantifiers-nested-04/main.c index 82def4f61ce..41d875577dd 100644 --- a/regression/contracts/quantifiers-nested-04/main.c +++ b/regression/contracts/quantifiers-nested-04/main.c @@ -1,14 +1,19 @@ // clang-format off -int f1(int *arr) __CPROVER_requires( - __CPROVER_forall { - int i; - (0 <= i && i < 10) ==> arr[i] == 0 - } || - arr[9] == -1 || - __CPROVER_exists { - int i; - (0 <= i && i < 10) && arr[i] == i - }) __CPROVER_ensures(__CPROVER_return_value == 0) +int f1(int *arr) + __CPROVER_requires( + __CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + } || + arr[9] == -1 || + __CPROVER_exists { + int i; + (0 <= i && i < 10) && arr[i] == i + } + ) + __CPROVER_ensures( + __CPROVER_return_value == 0 + ) // clang-format on { return 0; diff --git a/regression/contracts/quantifiers-nested-04/test.desc b/regression/contracts/quantifiers-nested-04/test.desc index 8bd89966cbb..4f92cb05f86 100644 --- a/regression/contracts/quantifiers-nested-04/test.desc +++ b/regression/contracts/quantifiers-nested-04/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -Verification: This test case checks the handling of both a forall expression and an exists expression nested within a disjunction. diff --git a/regression/contracts/quantifiers-nested-05/main.c b/regression/contracts/quantifiers-nested-05/main.c index 6aa20e2cc7f..f667b14b177 100644 --- a/regression/contracts/quantifiers-nested-05/main.c +++ b/regression/contracts/quantifiers-nested-05/main.c @@ -1,8 +1,14 @@ // clang-format off -int f1(int *arr) __CPROVER_requires(!__CPROVER_forall { - int i; - (0 <= i && i < 10) ==> arr[i] == 0 - }) __CPROVER_ensures(__CPROVER_return_value == 0) +int f1(int *arr) + __CPROVER_requires( + !__CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + } + ) + __CPROVER_ensures( + __CPROVER_return_value == 0 + ) // clang-format on { return 0; diff --git a/regression/contracts/quantifiers-nested-05/test.desc b/regression/contracts/quantifiers-nested-05/test.desc index ceb27f76675..674b9bfc0b4 100644 --- a/regression/contracts/quantifiers-nested-05/test.desc +++ b/regression/contracts/quantifiers-nested-05/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -Verification: This test case checks the handling of a forall expression nested within a negation. diff --git a/regression/contracts/quantifiers-nested-06/main.c b/regression/contracts/quantifiers-nested-06/main.c index 28d2bf24add..fda936fb03e 100644 --- a/regression/contracts/quantifiers-nested-06/main.c +++ b/regression/contracts/quantifiers-nested-06/main.c @@ -1,20 +1,31 @@ +#include + // clang-format off -int f1(int *arr) __CPROVER_requires( - (__CPROVER_forall { - int i; - (0 <= i && i < 10) ==> arr[i] == 0 - } ? __CPROVER_exists { - int i; - (0 <= i && i < 10) ==> arr[i] == 0 - } : 1 == 0) && - (__CPROVER_forall { - int i; - (0 <= i && i < 10) ==> arr[i] == i - } ? 1 == 0 : +int f1(int *arr) + __CPROVER_requires( + ( + __CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + } ? + __CPROVER_exists { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + } : false + ) && ( __CPROVER_forall { int i; - (0 <= i && i < 10) ==> arr[i] == 0 - })) __CPROVER_ensures(__CPROVER_return_value == 0) + (0 <= i && i < 10) ==> arr[i] == i + } ? false : + __CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + } + ) + ) + __CPROVER_ensures( + __CPROVER_return_value == 0 + ) // clang-format on { return 0; diff --git a/regression/contracts/quantifiers-nested-06/test.desc b/regression/contracts/quantifiers-nested-06/test.desc index c2485334e38..941828fdeca 100644 --- a/regression/contracts/quantifiers-nested-06/test.desc +++ b/regression/contracts/quantifiers-nested-06/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- +^warning: ignoring -- -Verification: This test case checks the handling of forall and exists expressions nested within ternary ITE expressions (condition ? true : false). From ea71d662e976e698d22e3937f1026df8ef203998 Mon Sep 17 00:00:00 2001 From: Saswat Padhi Date: Mon, 24 May 2021 18:56:18 -0400 Subject: [PATCH 2/2] Rename regression tests for clarity --- .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 24 files changed, 0 insertions(+), 0 deletions(-) rename regression/contracts/{quantifiers-exists-both-01 => quantifiers-exists-both-enforce}/main.c (100%) rename regression/contracts/{quantifiers-exists-both-01 => quantifiers-exists-both-enforce}/test.desc (100%) rename regression/contracts/{quantifiers-exists-both-02 => quantifiers-exists-both-replace}/main.c (100%) rename regression/contracts/{quantifiers-exists-both-02 => quantifiers-exists-both-replace}/test.desc (100%) rename regression/contracts/{quantifiers-exists-ensures-01 => quantifiers-exists-ensures-enforce}/main.c (100%) rename regression/contracts/{quantifiers-exists-ensures-01 => quantifiers-exists-ensures-enforce}/test.desc (100%) rename regression/contracts/{quantifiers-exists-ensures-02 => quantifiers-exists-ensures-replace}/main.c (100%) rename regression/contracts/{quantifiers-exists-ensures-02 => quantifiers-exists-ensures-replace}/test.desc (100%) rename regression/contracts/{quantifiers-exists-requires-01 => quantifiers-exists-requires-enforce}/main.c (100%) rename regression/contracts/{quantifiers-exists-requires-01 => quantifiers-exists-requires-enforce}/test.desc (100%) rename regression/contracts/{quantifiers-exists-requires-02 => quantifiers-exists-requires-replace}/main.c (100%) rename regression/contracts/{quantifiers-exists-requires-02 => quantifiers-exists-requires-replace}/test.desc (100%) rename regression/contracts/{quantifiers-forall-both-01 => quantifiers-forall-both-enforce}/main.c (100%) rename regression/contracts/{quantifiers-forall-both-01 => quantifiers-forall-both-enforce}/test.desc (100%) rename regression/contracts/{quantifiers-forall-both-02 => quantifiers-forall-both-replace}/main.c (100%) rename regression/contracts/{quantifiers-forall-both-02 => quantifiers-forall-both-replace}/test.desc (100%) rename regression/contracts/{quantifiers-forall-ensures-01 => quantifiers-forall-ensures-enforce}/main.c (100%) rename regression/contracts/{quantifiers-forall-ensures-01 => quantifiers-forall-ensures-enforce}/test.desc (100%) rename regression/contracts/{quantifiers-forall-ensures-02 => quantifiers-forall-ensures-replace}/main.c (100%) rename regression/contracts/{quantifiers-forall-ensures-02 => quantifiers-forall-ensures-replace}/test.desc (100%) rename regression/contracts/{quantifiers-forall-requires-01 => quantifiers-forall-requires-enforce}/main.c (100%) rename regression/contracts/{quantifiers-forall-requires-01 => quantifiers-forall-requires-enforce}/test.desc (100%) rename regression/contracts/{quantifiers-forall-requires-02 => quantifiers-forall-requires-replace}/main.c (100%) rename regression/contracts/{quantifiers-forall-requires-02 => quantifiers-forall-requires-replace}/test.desc (100%) diff --git a/regression/contracts/quantifiers-exists-both-01/main.c b/regression/contracts/quantifiers-exists-both-enforce/main.c similarity index 100% rename from regression/contracts/quantifiers-exists-both-01/main.c rename to regression/contracts/quantifiers-exists-both-enforce/main.c diff --git a/regression/contracts/quantifiers-exists-both-01/test.desc b/regression/contracts/quantifiers-exists-both-enforce/test.desc similarity index 100% rename from regression/contracts/quantifiers-exists-both-01/test.desc rename to regression/contracts/quantifiers-exists-both-enforce/test.desc diff --git a/regression/contracts/quantifiers-exists-both-02/main.c b/regression/contracts/quantifiers-exists-both-replace/main.c similarity index 100% rename from regression/contracts/quantifiers-exists-both-02/main.c rename to regression/contracts/quantifiers-exists-both-replace/main.c diff --git a/regression/contracts/quantifiers-exists-both-02/test.desc b/regression/contracts/quantifiers-exists-both-replace/test.desc similarity index 100% rename from regression/contracts/quantifiers-exists-both-02/test.desc rename to regression/contracts/quantifiers-exists-both-replace/test.desc diff --git a/regression/contracts/quantifiers-exists-ensures-01/main.c b/regression/contracts/quantifiers-exists-ensures-enforce/main.c similarity index 100% rename from regression/contracts/quantifiers-exists-ensures-01/main.c rename to regression/contracts/quantifiers-exists-ensures-enforce/main.c diff --git a/regression/contracts/quantifiers-exists-ensures-01/test.desc b/regression/contracts/quantifiers-exists-ensures-enforce/test.desc similarity index 100% rename from regression/contracts/quantifiers-exists-ensures-01/test.desc rename to regression/contracts/quantifiers-exists-ensures-enforce/test.desc diff --git a/regression/contracts/quantifiers-exists-ensures-02/main.c b/regression/contracts/quantifiers-exists-ensures-replace/main.c similarity index 100% rename from regression/contracts/quantifiers-exists-ensures-02/main.c rename to regression/contracts/quantifiers-exists-ensures-replace/main.c diff --git a/regression/contracts/quantifiers-exists-ensures-02/test.desc b/regression/contracts/quantifiers-exists-ensures-replace/test.desc similarity index 100% rename from regression/contracts/quantifiers-exists-ensures-02/test.desc rename to regression/contracts/quantifiers-exists-ensures-replace/test.desc diff --git a/regression/contracts/quantifiers-exists-requires-01/main.c b/regression/contracts/quantifiers-exists-requires-enforce/main.c similarity index 100% rename from regression/contracts/quantifiers-exists-requires-01/main.c rename to regression/contracts/quantifiers-exists-requires-enforce/main.c diff --git a/regression/contracts/quantifiers-exists-requires-01/test.desc b/regression/contracts/quantifiers-exists-requires-enforce/test.desc similarity index 100% rename from regression/contracts/quantifiers-exists-requires-01/test.desc rename to regression/contracts/quantifiers-exists-requires-enforce/test.desc diff --git a/regression/contracts/quantifiers-exists-requires-02/main.c b/regression/contracts/quantifiers-exists-requires-replace/main.c similarity index 100% rename from regression/contracts/quantifiers-exists-requires-02/main.c rename to regression/contracts/quantifiers-exists-requires-replace/main.c diff --git a/regression/contracts/quantifiers-exists-requires-02/test.desc b/regression/contracts/quantifiers-exists-requires-replace/test.desc similarity index 100% rename from regression/contracts/quantifiers-exists-requires-02/test.desc rename to regression/contracts/quantifiers-exists-requires-replace/test.desc diff --git a/regression/contracts/quantifiers-forall-both-01/main.c b/regression/contracts/quantifiers-forall-both-enforce/main.c similarity index 100% rename from regression/contracts/quantifiers-forall-both-01/main.c rename to regression/contracts/quantifiers-forall-both-enforce/main.c diff --git a/regression/contracts/quantifiers-forall-both-01/test.desc b/regression/contracts/quantifiers-forall-both-enforce/test.desc similarity index 100% rename from regression/contracts/quantifiers-forall-both-01/test.desc rename to regression/contracts/quantifiers-forall-both-enforce/test.desc diff --git a/regression/contracts/quantifiers-forall-both-02/main.c b/regression/contracts/quantifiers-forall-both-replace/main.c similarity index 100% rename from regression/contracts/quantifiers-forall-both-02/main.c rename to regression/contracts/quantifiers-forall-both-replace/main.c diff --git a/regression/contracts/quantifiers-forall-both-02/test.desc b/regression/contracts/quantifiers-forall-both-replace/test.desc similarity index 100% rename from regression/contracts/quantifiers-forall-both-02/test.desc rename to regression/contracts/quantifiers-forall-both-replace/test.desc diff --git a/regression/contracts/quantifiers-forall-ensures-01/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c similarity index 100% rename from regression/contracts/quantifiers-forall-ensures-01/main.c rename to regression/contracts/quantifiers-forall-ensures-enforce/main.c diff --git a/regression/contracts/quantifiers-forall-ensures-01/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc similarity index 100% rename from regression/contracts/quantifiers-forall-ensures-01/test.desc rename to regression/contracts/quantifiers-forall-ensures-enforce/test.desc diff --git a/regression/contracts/quantifiers-forall-ensures-02/main.c b/regression/contracts/quantifiers-forall-ensures-replace/main.c similarity index 100% rename from regression/contracts/quantifiers-forall-ensures-02/main.c rename to regression/contracts/quantifiers-forall-ensures-replace/main.c diff --git a/regression/contracts/quantifiers-forall-ensures-02/test.desc b/regression/contracts/quantifiers-forall-ensures-replace/test.desc similarity index 100% rename from regression/contracts/quantifiers-forall-ensures-02/test.desc rename to regression/contracts/quantifiers-forall-ensures-replace/test.desc diff --git a/regression/contracts/quantifiers-forall-requires-01/main.c b/regression/contracts/quantifiers-forall-requires-enforce/main.c similarity index 100% rename from regression/contracts/quantifiers-forall-requires-01/main.c rename to regression/contracts/quantifiers-forall-requires-enforce/main.c diff --git a/regression/contracts/quantifiers-forall-requires-01/test.desc b/regression/contracts/quantifiers-forall-requires-enforce/test.desc similarity index 100% rename from regression/contracts/quantifiers-forall-requires-01/test.desc rename to regression/contracts/quantifiers-forall-requires-enforce/test.desc diff --git a/regression/contracts/quantifiers-forall-requires-02/main.c b/regression/contracts/quantifiers-forall-requires-replace/main.c similarity index 100% rename from regression/contracts/quantifiers-forall-requires-02/main.c rename to regression/contracts/quantifiers-forall-requires-replace/main.c diff --git a/regression/contracts/quantifiers-forall-requires-02/test.desc b/regression/contracts/quantifiers-forall-requires-replace/test.desc similarity index 100% rename from regression/contracts/quantifiers-forall-requires-02/test.desc rename to regression/contracts/quantifiers-forall-requires-replace/test.desc