Fixed contracts-dfcc regressions

esteffin · esteffin · commit 520b5065f23c · 2023-12-19T17:14:42.000Z
diff --git a/regression/contracts-dfcc/assigns-local-composite/test.desc b/regression/contracts-dfcc/assigns-local-composite/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/assigns-replace-ignored-return-value/test.desc b/regression/contracts-dfcc/assigns-replace-ignored-return-value/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+--dfcc main --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/assigns_enforce_15/test-foo.desc b/regression/contracts-dfcc/assigns_enforce_15/test-foo.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts-dfcc/assigns_enforce_16/test.desc b/regression/contracts-dfcc/assigns_enforce_16/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo _ --pointer-primitive-check
+--dfcc main --enforce-contract foo _ --pointer-primitive-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/assigns_enforce_17/test.desc b/regression/contracts-dfcc/assigns_enforce_17/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract pure
+--dfcc main --enforce-contract pure _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$
diff --git a/regression/contracts-dfcc/assigns_enforce_23/test.desc b/regression/contracts-dfcc/assigns_enforce_23/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/assigns_enforce_functions_in_contracts/test.desc b/regression/contracts-dfcc/assigns_enforce_functions_in_contracts/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/assigns_enforce_malloc_01/test.desc b/regression/contracts-dfcc/assigns_enforce_malloc_01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract f
+--dfcc main --enforce-contract f _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f\.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS
diff --git a/regression/contracts-dfcc/assigns_enforce_malloc_03/test.desc b/regression/contracts-dfcc/assigns_enforce_malloc_03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 ^\[foo.assigns.\d+\].* Check that \*loc1 is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that \*loc2 is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/assigns_enforce_offsets_3/test.desc b/regression/contracts-dfcc/assigns_enforce_offsets_3/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/assigns_enforce_structs_01/test.desc b/regression/contracts-dfcc/assigns_enforce_structs_01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract f
+--dfcc main --enforce-contract f _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
diff --git a/regression/contracts-dfcc/assigns_enforce_structs_02/test.desc b/regression/contracts-dfcc/assigns_enforce_structs_02/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract f
+--dfcc main --enforce-contract f _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
diff --git a/regression/contracts-dfcc/assigns_enforce_structs_03/test.desc b/regression/contracts-dfcc/assigns_enforce_structs_03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract f
+--dfcc main --enforce-contract f _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/assigns_replace_03/test.desc b/regression/contracts-dfcc/assigns_replace_03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --replace-call-with-contract bar _ --pointer-primitive-check
+--dfcc main --replace-call-with-contract bar _ --pointer-primitive-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/enforce.desc b/regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/enforce.desc
@@ -1,6 +1,6 @@
 CORE
 main_enforce.c
---dfcc main --enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+--dfcc main --enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --no-standard-checks
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts-dfcc/detect_loop_locals/test.desc b/regression/contracts-dfcc/detect_loop_locals/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^\[main.assigns.\d+\].*line 10 Check that i is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts-dfcc/function-calls-05-function-pointer-call-pass/test.desc b/regression/contracts-dfcc/function-calls-05-function-pointer-call-pass/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 \[foo.postcondition.\d+\] line \d+ Check ensures clause of contract contract::foo for function foo: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
diff --git a/regression/contracts-dfcc/github_6168_infinite_unwinding_bug/test.desc b/regression/contracts-dfcc/github_6168_infinite_unwinding_bug/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/history-index/test.desc b/regression/contracts-dfcc/history-index/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/history-index/test_contracts_file.desc b/regression/contracts-dfcc/history-index/test_contracts_file.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---loop-contracts-file test.json --dfcc main --apply-loop-contracts
+--loop-contracts-file test.json --dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/history-pointer-enforce-01/test.desc b/regression/contracts-dfcc/history-pointer-enforce-01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/history-pointer-enforce-08/test.desc b/regression/contracts-dfcc/history-pointer-enforce-08/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/history-pointer-enforce-09/test.desc b/regression/contracts-dfcc/history-pointer-enforce-09/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo
+--dfcc main --enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$
diff --git a/regression/contracts-dfcc/invar_check_multiple_loops/test.desc b/regression/contracts-dfcc/invar_check_multiple_loops/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$
diff --git a/regression/contracts-dfcc/invar_check_nested_loops/test.desc b/regression/contracts-dfcc/invar_check_nested_loops/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$
diff --git a/regression/contracts-dfcc/invar_loop-entry_check/test.desc b/regression/contracts-dfcc/invar_loop-entry_check/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts _ --pointer-primitive-check
+--dfcc main --apply-loop-contracts _ --pointer-primitive-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.loop_assigns.\d+] line 14 Check assigns clause inclusion for loop .*: SUCCESS$
diff --git a/regression/contracts-dfcc/is_fresh_indirect_calls/test.desc b/regression/contracts-dfcc/is_fresh_indirect_calls/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --replace-call-with-contract foo
+--dfcc main --replace-call-with-contract foo _ --no-standard-checks
 ^\[main.assertion.\d+\].*c is rw_ok: SUCCESS$
 ^\[main.assertion.\d+\].*c and a are distinct: SUCCESS$
 ^\[main.assertion.\d+\].*c and b are distinct: SUCCESS$
diff --git a/regression/contracts-dfcc/is_unique_01_replace/test.desc b/regression/contracts-dfcc/is_unique_01_replace/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --replace-call-with-contract foo
+--dfcc main --replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/loop_assigns-05/test.desc b/regression/contracts-dfcc/loop_assigns-05/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
diff --git a/regression/contracts-dfcc/loop_assigns-slice-assignable-ptr/test.desc b/regression/contracts-dfcc/loop_assigns-slice-assignable-ptr/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.loop_assigns.\d+\] line 24 Check assigns clause inclusion for loop .*: SUCCESS$
diff --git a/regression/contracts-dfcc/loop_assigns_scoped_local_statics/test.desc b/regression/contracts-dfcc/loop_assigns_scoped_local_statics/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
diff --git a/regression/contracts-dfcc/loop_assigns_scoped_local_statics_propagate/test.desc b/regression/contracts-dfcc/loop_assigns_scoped_local_statics_propagate/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --replace-call-with-contract bar --apply-loop-contracts
+--dfcc main --replace-call-with-contract bar --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.loop_assigns.\d+\] line 33 Check assigns clause inclusion for loop .*: SUCCESS$
diff --git a/regression/contracts-dfcc/loop_contracts_memcmp/test.desc b/regression/contracts-dfcc/loop_contracts_memcmp/test.desc
@@ -1,6 +1,6 @@
 CORE gcc-only
 main.c
---dfcc main --apply-loop-contracts
+--dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/loop_contracts_memcmp/test_contracts_file.desc b/regression/contracts-dfcc/loop_contracts_memcmp/test_contracts_file.desc
@@ -1,6 +1,6 @@
 CORE gcc-only
 main.c
---loop-contracts-file test.json --dfcc main --apply-loop-contracts
+--loop-contracts-file test.json --dfcc main --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/quantifiers-exists-both-replace/test.desc b/regression/contracts-dfcc/quantifiers-exists-both-replace/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --replace-call-with-contract f1
+--dfcc main --replace-call-with-contract f1 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$
diff --git a/regression/contracts-dfcc/quantifiers-exists-ensures-replace/test.desc b/regression/contracts-dfcc/quantifiers-exists-ensures-replace/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --replace-call-with-contract f1
+--dfcc main --replace-call-with-contract f1 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.1\] line .* assertion len > 0 ==> found_zero: SUCCESS$
diff --git a/regression/contracts-dfcc/quantifiers-exists-requires-enforce/test.desc b/regression/contracts-dfcc/quantifiers-exists-requires-enforce/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract f1
+--dfcc main --enforce-contract f1 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::f1 for function f1)?: SUCCESS$
diff --git a/regression/contracts-dfcc/quantifiers-forall-both-replace/test.desc b/regression/contracts-dfcc/quantifiers-forall-both-replace/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --replace-call-with-contract f1
+--dfcc main --replace-call-with-contract f1 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$
diff --git a/regression/contracts-dfcc/quantifiers-forall-requires-replace/test.desc b/regression/contracts-dfcc/quantifiers-forall-requires-replace/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --replace-call-with-contract f1
+--dfcc main --replace-call-with-contract f1 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$
diff --git a/regression/contracts-dfcc/test_array_memory_replace/test.desc b/regression/contracts-dfcc/test_array_memory_replace/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --replace-call-with-contract foo
+--dfcc main --replace-call-with-contract foo _ --no-standard-checks
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts-dfcc/test_possibly_aliased_arguments/test.desc b/regression/contracts-dfcc/test_possibly_aliased_arguments/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --replace-call-with-contract sub_ptr_values
+--dfcc main --replace-call-with-contract sub_ptr_values _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[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$
diff --git a/regression/contracts-dfcc/test_scalar_memory_replace/test.desc b/regression/contracts-dfcc/test_scalar_memory_replace/test.desc
@@ -1,6 +1,6 @@
 CORE dfcc-only
 main.c
---dfcc main --replace-call-with-contract foo
+--dfcc main --replace-call-with-contract foo _ --no-standard-checks
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts-dfcc/test_struct_replace/test.desc b/regression/contracts-dfcc/test_struct_replace/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --replace-call-with-contract foo
+--dfcc main --replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[foo.precondition.\d+\] line \d+ Check requires clause of (contract contract::foo for function foo|foo in main): SUCCESS$
