Fixed contracts regressions

Author: esteffin

regression/contracts/assigns-replace-ignored-return-value/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo _ --no-standard-checks
 ^\[bar.precondition.\d+\] line \d+ Check requires clause of bar in foo: SUCCESS$
 ^\[baz.precondition.\d+\] line \d+ Check requires clause of baz in foo: SUCCESS$
 ^EXIT=0$

regression/contracts/assigns_enforce_21/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo --replace-call-with-contract quz
+--enforce-contract foo --replace-call-with-contract quz _ --no-standard-checks
 ^\[foo.assigns.\d+\] line \d+ Check that \*y is valid: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[bar.assigns.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE$

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2
+--enforce-contract f1 --enforce-contract f2 _ --no-standard-checks
 ^\[f1.assigns.\d+\] line 6 Check that \*a is valid: SUCCESS$
 ^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$
 ^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$

regression/contracts/assigns_enforce_havoc_object/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo
+--enforce-contract foo _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_object_whole\(\(.*\)a1->u.b->c\) is valid: SUCCESS$

regression/contracts/assigns_enforce_multi_file_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f1 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.assigns.\d+\] line \d+ Check that \*a is valid: SUCCESS$

regression/contracts/assigns_enforce_scoping_02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f1 _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.assigns.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$

regression/contracts/assigns_enforce_statics/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo _ --pointer-primitive-check
+--enforce-contract foo _ --pointer-primitive-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[foo.assigns.\d+\] line \d+ Check that x is valid: SUCCESS$

regression/contracts/assigns_enforce_structs_06/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2 --enforce-contract f3
+--enforce-contract f1 --enforce-contract f2 --enforce-contract f3 _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$

regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc

@@ -1,6 +1,6 @@
 CORE
 main_enforce.c
---enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --no-standard-checks
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/contracts/assigns_type_checking_valid_cases/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check
+--enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[foo10.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$

regression/contracts/detect_loop_locals/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^\[main.assigns.\d+\].*line 10 Check that i is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$

regression/contracts/github_6168_infinite_unwinding_bug/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/history-index/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/history-pointer-enforce-10/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo --enforce-contract bar --enforce-contract baz
+--enforce-contract foo --enforce-contract bar --enforce-contract baz _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[bar.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$

regression/contracts/history-pointer-replace-04/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$

regression/contracts/invar_check_multiple_loops/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_nested_loops/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_pointer_modifies-01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts --pointer-check
+--apply-loop-contracts --pointer-check _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_check_pointer_modifies-02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts --pointer-check
+--apply-loop-contracts --pointer-check _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_dynamic_array/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invar_loop-entry_check/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts _ --pointer-primitive-check
+--apply-loop-contracts _ --pointer-primitive-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/invariant_side_effects/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/is_unique_01_replace/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/loop_assigns-01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/loop_assigns-03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/loop_assigns-05/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$

regression/contracts/loop_assigns-slice-assignable-ptr/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/loop_assigns-slice-assignable-scalar/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/loop_assigns-slice-from/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/loop_assigns-slice-upto-fail/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$

regression/contracts/loop_assigns-slice-upto-pass/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$

regression/contracts/loop_assigns_inference-01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$

regression/contracts/loop_assigns_inference-02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/loop_assigns_scoped_local_statics/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$

regression/contracts/loop_assigns_scoped_local_statics_propagate/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract bar --apply-loop-contracts
+--replace-call-with-contract bar --apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assigns.\d+\] line \d+ Check that j \(assigned by the contract of bar\) is assignable: SUCCESS$

regression/contracts/no_redudant_checks/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---pointer-overflow-check _ --pointer-overflow-check --unsigned-overflow-check
+--pointer-overflow-check _ --pointer-overflow-check --unsigned-overflow-check --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[malloc.assertion.1\].*: SUCCESS

regression/contracts/nonvacuous_loop_contracts/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts _ --signed-overflow-check --unsigned-overflow-check
+--apply-loop-contracts _ --signed-overflow-check --unsigned-overflow-check --no-standard-checks
 \[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
 \[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
 \[main.assigns.\d+\] line \d+ Check that end is valid: SUCCESS$

regression/contracts/quantifiers-forall-ensures-enforce/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f1 _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$

regression/contracts/quantifiers-loop-02/test.desc

@@ -1,6 +1,6 @@
 CORE smt-backend broken-cprover-smt-backend thorough-smt-backend
 main.c
---apply-loop-contracts _ --z3
+--apply-loop-contracts _ --z3 --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS$

regression/contracts/quantifiers-loop-03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---apply-loop-contracts
+--apply-loop-contracts _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$

regression/contracts/test_aliasing_ensure/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo
+--enforce-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS

regression/contracts/test_array_memory_replace/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS

regression/contracts/test_array_memory_too_small_replace/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=10$
 ^SIGNAL=0$
 \[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: FAILURE

regression/contracts/test_scalar_memory_replace/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo
+--replace-call-with-contract foo _ --no-standard-checks
 ^EXIT=0$
 ^SIGNAL=0$
 \[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS