Skip to content

Commit 205e123

Browse files
tautschnigtautschnig
committed
De-duplicate contracts regression tests (part 2)
Removal of duplicates based on a manual review of the diff between test directories of the same name.
1 parent 01fd5ea commit 205e123

File tree

82 files changed

+50
-1365
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

82 files changed

+50
-1365
lines changed

‎regression/contracts-dfcc/assigns-local-composite/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
^EXIT=0$

‎regression/contracts-dfcc/assigns_enforce_functions_in_contracts/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
^EXIT=0$

‎regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/enforce.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE dfcc-only
1+
CORE
22
main_enforce.c
33
--dfcc main --enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
44
^VERIFICATION SUCCESSFUL$

‎regression/contracts-dfcc/assigns_validity_pointer_02/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
6+
^\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$
77
^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
88
^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
99
^\[baz.assigns.\d+\] line \d+ Check that \*z is assignable: SUCCESS$

‎regression/contracts-dfcc/function_check_01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract min
44
^EXIT=0$

‎regression/contracts-dfcc/function_check_03/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG dfcc-only
1+
KNOWNBUG
22
main.c
33
--dfcc main --check-code-contracts
44
^EXIT=0$

‎regression/contracts-dfcc/function_check_04/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG dfcc-only
1+
KNOWNBUG
22
main.c
33
--dfcc main --apply-code-contracts
44
^EXIT=10$

‎regression/contracts-dfcc/function_check_05/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG dfcc-only
1+
KNOWNBUG
22
main.c
33
--dfcc main --check-code-contracts
44
^EXIT=0$

‎regression/contracts-dfcc/function_check_mem_01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG dfcc-only
1+
KNOWNBUG
22
main.c
33
--dfcc main --check-code-contracts
44
^EXIT=0$

‎regression/contracts-dfcc/history-pointer-enforce-09/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[foo.postcondition.\d+\] line \d+ Check ensures clause of contract contract::foo for function foo: SUCCESS$
6+
^\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$
77
^\[foo.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
88
^VERIFICATION SUCCESSFUL$
99
--

‎regression/contracts-dfcc/is_fresh_indirect_calls/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract foo
44
^\[main.assertion.\d+\].*c is rw_ok: SUCCESS$

‎regression/contracts-dfcc/quantifiers-exists-both-enforce/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.postcondition.\d+\] line \d+ Check ensures clause of contract contract::f1 for function f1: SUCCESS$
6+
^\[f1.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::f1 for function f1)?: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/contracts-dfcc/quantifiers-exists-both-replace/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.precondition.\d+\] line \d+ Check requires clause of contract contract::f1 for function f1: SUCCESS$
6+
^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/contracts-dfcc/quantifiers-exists-requires-enforce/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.postcondition.\d+\] line \d+ Check ensures clause of contract contract::f1 for function f1: SUCCESS$
6+
^\[f1.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::f1 for function f1)?: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/contracts-dfcc/quantifiers-exists-requires-replace/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract f1 --replace-call-with-contract f2
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[f1.precondition.\d+\] line \d+ Check requires clause of contract contract::f1 for function f1: SUCCESS$
7-
^\[f2.precondition.\d+\] line \d+ Check requires clause of contract contract::f2 for function f2: FAILURE$
6+
^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$
7+
^\[f2.precondition.\d+\] line \d+ Check requires clause of (contract contract::f2 for function f2|f2 in main): FAILURE$
88
^VERIFICATION FAILED$
99
--
1010
^warning: ignoring

‎regression/contracts-dfcc/quantifiers-forall-both-enforce/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.postcondition.\d+\] line \d+ Check ensures clause of contract contract::f1 for function f1: SUCCESS$
6+
^\[f1.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::f1 for function f1)?: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/contracts-dfcc/quantifiers-forall-both-replace/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.precondition.\d+\] line \d+ Check requires clause of contract contract::f1 for function f1: SUCCESS$
6+
^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/contracts-dfcc/quantifiers-forall-requires-enforce/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.postcondition.\d+\] line \d+ Check ensures clause of contract contract::f1 for function f1: SUCCESS$
6+
^\[f1.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::f1 for function f1)?: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/contracts-dfcc/quantifiers-forall-requires-replace/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[f1.precondition.\d+\] line \d+ Check requires clause of contract contract::f1 for function f1: SUCCESS$
6+
^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring
1010
--
1111
The purpose of this test is to ensure that we can safely use __CPROVER_forall
1212
within positive contexts (replaced REQUIRES clauses).
1313

14-
This is fully supported (without requiring full unrolling) with the SAT backend.
14+
This is fully supported (without requiring full unrolling) with the SAT backend.

‎regression/contracts-dfcc/replace-nondet-return-value/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract cmp
44
^EXIT=10$

‎regression/contracts-dfcc/test_aliasing_replace/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract foo
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[foo.precondition.\d+\] line \d+ Check requires clause of contract contract::foo for function foo: FAILURE$
6+
^\[foo.precondition.\d+\] line \d+ Check requires clause of (contract contract::foo for function foo|foo in main): FAILURE$
77
^\[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS$
88
^VERIFICATION FAILED$
99
--

‎regression/contracts-dfcc/test_array_memory_enforce/test.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
6-
\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS
7-
\[foo.assigns.\d+\].*Check that \*x is assignable: SUCCESS
8-
\[foo.assigns.\d+\].*Check that x\[\(.* int\)5\] is assignable: SUCCESS
9-
\[foo.assigns.\d+\].*Check that x\[\(.* int\)9\] is assignable: SUCCESS
6+
\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS
7+
\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
8+
\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS
9+
\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS
1010
^VERIFICATION SUCCESSFUL$
1111
--
1212
--

‎regression/contracts-dfcc/test_possibly_aliased_arguments/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract sub_ptr_values
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[sub_ptr_values.precondition.\d+\] line \d+ Check requires clause of contract contract::sub_ptr_values for function sub_ptr_values: SUCCESS$
6+
^\[sub_ptr_values.precondition.\d+\] line \d+ Check requires clause of (contract contract::sub_ptr_values for function sub_ptr_values|sub_ptr_values in main): SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
--
99
--

‎regression/contracts-dfcc/test_scalar_memory_enforce/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract foo
4-
\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS
5-
\[foo.assigns.\d+\].*Check that \*x is assignable: SUCCESS
4+
\[foo.postcondition.\d+\].*Check ensures clause( of contract contract::foo for function foo)?: SUCCESS
5+
\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS
66
^VERIFICATION SUCCESSFUL$
77
^EXIT=0$
88
^SIGNAL=0$

‎regression/contracts-dfcc/test_struct_enforce/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
6-
\[foo.postcondition.\d+\] line \d+ Check ensures clause of contract contract::foo for function foo: SUCCESS$
6+
\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$
77
\[foo.assigns.\d+\] line \d+ Check that x->baz is assignable: SUCCESS
88
\[foo.assigns.\d+\] line \d+ Check that x->qux is assignable: SUCCESS
99
\[main.assertion.\d+\] line \d+ assertion rval \=\= 10: SUCCESS

‎regression/contracts-dfcc/test_struct_member_enforce/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
6-
\[foo.postcondition.\d+\] line \d+ Check ensures clause of contract contract::foo for function foo: SUCCESS$
6+
\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$
77
\[foo.assigns.\d+\] line \d+ Check that x->str\[\(.*\)\(x->len - 1\)\] is assignable: SUCCESS
88
\[main.assertion.\d+\] line \d+ assertion rval \=\= 128: SUCCESS
99
^VERIFICATION SUCCESSFUL$

‎regression/contracts-dfcc/test_struct_replace/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
1-
CORE dfcc-only
1+
CORE
22
main.c
33
--dfcc main --replace-call-with-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[foo.precondition.\d+\] line \d+ Check requires clause of contract contract::foo for function foo: SUCCESS$
6+
^\[foo.precondition.\d+\] line \d+ Check requires clause of (contract contract::foo for function foo|foo in main): SUCCESS$
77
^\[main.assertion.\d+\] line \d+ assertion rval \=\= x->baz \+ x->qux: SUCCESS$
88
^\[main.assertion.\d+\] line \d+ assertion \*x \=\= \*y: SUCCESS$
99
^VERIFICATION SUCCESSFUL$

‎regression/contracts/assigns-local-composite/main.c

Lines changed: 0 additions & 104 deletions
This file was deleted.

‎regression/contracts/assigns-local-composite/test.desc

Lines changed: 0 additions & 12 deletions
This file was deleted.

0 commit comments

Comments
 (0)