Skip to content

Commit 58f05d9

Browse files
author
Enrico Steffinlongo
committed
Added --no-malloc-may-fail from last failing tests of contracts-dfcc
1 parent 24f890e commit 58f05d9

File tree

72 files changed

+72
-72
lines changed

Some content is hidden

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

72 files changed

+72
-72
lines changed

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract foo _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_16/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract foo _ --pointer-primitive-check --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo _ --pointer-primitive-check --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_21/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo --replace-call-with-contract quz
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo --replace-call-with-contract quz
44
^\[bar.assigns.\d+\].*Check that \*y is assignable: SUCCESS$
55
^VERIFICATION FAILED$
66
^EXIT=10$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_23/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract foo _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_arrays_02/test-f1.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract f1
3+
--no-malloc-may-fail --dfcc main --enforce-contract f1
44
^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$
55
^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$
66
^EXIT=10$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_arrays_02/test-f2.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract f2
3+
--no-malloc-may-fail --dfcc main --enforce-contract f2
44
^\[f2.assigns.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
55
^\[f2.assigns.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$
66
^EXIT=0$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_malloc_01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract f _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract f _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[f\.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS

Diff for: ‎regression/contracts-dfcc/assigns_enforce_malloc_02/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract f
3+
--no-malloc-may-fail --dfcc main --enforce-contract f
44
main.c function f
55
^\[f.assigns.\d+\] line 7 Check that ptr is assignable: SUCCESS$
66
^\[f.assigns.\d+\] line 12 Check that \*ptr is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_malloc_03/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract foo _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo _ --no-standard-checks
44
^\[foo.assigns.\d+\].* Check that \*loc1 is assignable: SUCCESS$
55
^\[foo.assigns.\d+\].* Check that \*loc2 is assignable: SUCCESS$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_multi_file_02/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract f1
3+
--no-malloc-may-fail --dfcc main --enforce-contract f1
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_offsets_3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract foo _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_structs_01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract f _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract f _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[f.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_structs_02/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract f _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract f _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[f.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_structs_03/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract f _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract f _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract f1
3+
--no-malloc-may-fail --dfcc main --enforce-contract f1
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_enforce_structs_06/test-f3.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract f3
3+
--no-malloc-may-fail --dfcc main --enforce-contract f3
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[f3.assigns.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_replace_03/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --replace-call-with-contract bar _ --pointer-primitive-check --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --replace-call-with-contract bar _ --pointer-primitive-check --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/enforce.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main_enforce.c
3-
--dfcc main --enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --no-standard-checks
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

Diff for: ‎regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_pass/enforce.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main_enforce.c
3-
--dfcc main --enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo1.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo1 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo1 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo10.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo10 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo10 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo10.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo2.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo2 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo2 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo3.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo3 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo3 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo3.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo4.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo4 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo4 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo4.assigns.\d+\] line \d+ Check that \*c is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo5.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo5 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo5 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo6.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo6 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo6 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo6.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo7.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo7 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo7 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo7.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo8.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo8 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo8 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?0\] is assignable: SUCCESS$

Diff for: ‎regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo9.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo9 _ --pointer-primitive-check
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo9 _ --pointer-primitive-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

Diff for: ‎regression/contracts-dfcc/frees-clause-and-predicates/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

Diff for: ‎regression/contracts-dfcc/history-pointer-enforce-08/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract foo _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --enforce-contract foo _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$

Diff for: ‎regression/contracts-dfcc/history-pointer-enforce-10/test-bar.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract bar
3+
--no-malloc-may-fail --dfcc main --enforce-contract bar
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[bar.postcondition.\d+\] line \d+ Check ensures clause of contract contract::bar for function bar: SUCCESS$

Diff for: ‎regression/contracts-dfcc/history-pointer-enforce-10/test-baz.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract baz
3+
--no-malloc-may-fail --dfcc main --enforce-contract baz
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[baz.postcondition.\d+\] line \d+ Check ensures clause of contract contract::baz for function baz: SUCCESS$

Diff for: ‎regression/contracts-dfcc/history-pointer-enforce-10/test-foo.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --enforce-contract foo
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo.postcondition.\d+\] line \d+ Check ensures clause of contract contract::foo for function foo: SUCCESS$

Diff for: ‎regression/contracts-dfcc/invar_check_pointer_modifies-01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts --pointer-check
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts --pointer-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+\] line 10 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/invar_check_pointer_modifies-02/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts --pointer-check
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts --pointer-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/invar_havoc_dynamic_array/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+\] line 11 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+\] line 19 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/invar_loop-entry_check/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts _ --pointer-primitive-check --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts _ --pointer-primitive-check --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+] line 14 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/invariant_side_effects/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/is_fresh_indirect_calls/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--dfcc main --replace-call-with-contract foo _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --replace-call-with-contract foo _ --no-standard-checks
44
^\[main.assertion.\d+\].*c is rw_ok: SUCCESS$
55
^\[main.assertion.\d+\].*c and a are distinct: SUCCESS$
66
^\[main.assertion.\d+\].*c and b are distinct: SUCCESS$

Diff for: ‎regression/contracts-dfcc/loop_assigns-01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[foo.loop_assigns.\d+\] line 22 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/loop_assigns-03/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+\] line 17 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/loop_assigns-slice-assignable-ptr/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts _ --no-standard-checks
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+\] line 24 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/loop_assigns-slice-assignable-scalar/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/loop_assigns-slice-from/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$
55
^\[main.loop_invariant_base.\d+\] line 21 Check invariant before entry for loop .*: SUCCESS$
66
^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$

Diff for: ‎regression/contracts-dfcc/loop_assigns-slice-upto-pass/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--dfcc main --apply-loop-contracts
3+
--no-malloc-may-fail --dfcc main --apply-loop-contracts
44
^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$
55
^\[main.loop_invariant_base.\d+\] line 21 Check invariant before entry for loop .*: SUCCESS$
66
^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$

0 commit comments

Comments
 (0)