CONTRACTS: deduplicate tests

Author: Remi Delmas

regression/contracts-dfcc/invar_function-old_fail/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --apply-loop-contracts
 ^main.c.* error: __CPROVER_old is not allowed in loop invariants.$

regression/contracts-dfcc/variant_function_call_fail/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --apply-loop-contracts
 ^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$
@@ -8,7 +8,7 @@ main.c
 --
 This test fails because the decreases clause contains a function call. Decreases
 clauses must not contain loops, since we want to ensure that the
-calculation of decreases clauses will terminate. To enforce this requirement, 
-for now, we simply ban decreases clauses from containing function calls. 
+calculation of decreases clauses will terminate. To enforce this requirement,
+for now, we simply ban decreases clauses from containing function calls.
 In the future, we may allow function calls (but definitely not loops) to appear
-inside decreases clauses. 
+inside decreases clauses.

regression/contracts-dfcc/variant_parsing_multiple_clauses_fail/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --apply-loop-contracts
 activate-multi-line-match
@@ -12,5 +12,5 @@ This test fails because we have multiple decreases clauses. CBMC only admits
 one decreases clause for each loop. If one wants to write a multidimensional
 decreases clause, it should be placed inside a single __CPROVER_decreases(...),
 where each component of the multidimensional decreases clause is separated by a
-comma. Hence, in this test, the correct syntax is 
+comma. Hence, in this test, the correct syntax is
 __CPROVER_decreases(N - i, 42).

regression/contracts-dfcc/variant_parsing_statement_fail/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --apply-loop-contracts
 activate-multi-line-match
@@ -8,6 +8,6 @@ activate-multi-line-match
 ^SIGNAL=0$
 --
 --
-This test fails because the decreases clause is a statement (more precisely, 
+This test fails because the decreases clause is a statement (more precisely,
 an assignment) rather than an expression (more precisely, an ACSL binding
 expression).

regression/contracts-dfcc/variant_side_effects_fail/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+CORE
 main.c
 --dfcc main --apply-loop-contracts
 ^Decreases clause is not side-effect free. \(at: file main.c line .* function main\)$
@@ -8,6 +8,6 @@ main.c
 --
 This test fails because the decreases clause contains a side effect, namely
 incrementing variable N by zero. In this case, although the value of N
-remains unchanged after the increment operation, we read from and write to N. 
-So this constitues a side effect. Decreases clauses are banned from containing 
-side effects, since decreases clauses should not modify program states. 
+remains unchanged after the increment operation, we read from and write to N.
+So this constitues a side effect. Decreases clauses are banned from containing
+side effects, since decreases clauses should not modify program states.