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.

Author: tautschnig

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

@@ -1,4 +1,4 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --enforce-contract foo
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_functions_in_contracts/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --enforce-contract foo
 ^EXIT=0$

regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/enforce.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+CORE
 main_enforce.c
 --dfcc main --enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
 ^VERIFICATION SUCCESSFUL$

regression/contracts-dfcc/assigns_validity_pointer_02/test.desc

@@ -1,9 +1,9 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
+^\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[baz.assigns.\d+\] line \d+ Check that \*z is assignable: SUCCESS$

regression/contracts-dfcc/function_check_01/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --replace-call-with-contract min
 ^EXIT=0$

regression/contracts-dfcc/function_check_03/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG dfcc-only
+KNOWNBUG
 main.c
 --dfcc main --check-code-contracts
 ^EXIT=0$

regression/contracts-dfcc/function_check_04/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG dfcc-only
+KNOWNBUG
 main.c
 --dfcc main --apply-code-contracts
 ^EXIT=10$

regression/contracts-dfcc/function_check_05/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG dfcc-only
+KNOWNBUG
 main.c
 --dfcc main --check-code-contracts
 ^EXIT=0$

regression/contracts-dfcc/function_check_mem_01/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG dfcc-only
+KNOWNBUG
 main.c
 --dfcc main --check-code-contracts
 ^EXIT=0$

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

@@ -1,9 +1,9 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-^\[foo.postcondition.\d+\] line \d+ Check ensures clause of contract contract::foo for function foo: SUCCESS$
+^\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$
 ^\[foo.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --