Skip to content

Commit acb58e7

Browse files
authored
Merge pull request #7051 from diffblue/shortcircuit2
Simplify goto-program generated for short-circuit operators
2 parents 23045d1 + 1570e0a commit acb58e7

File tree

15 files changed

+50
-43
lines changed

15 files changed

+50
-43
lines changed

regression/cbmc-cover/Quantifiers-not-exists/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--cover location
44
^\*\* 1 of 46 covered \(2.2%\)

regression/cbmc/Quantifiers-not-exists/fixed.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ fixed.c
33

44
^\*\* Results:$
55
^\[main.assertion.5\] line 31 assertion a\[.*\]\[.*\] > 10: SUCCESS$
6-
^\[main.assertion.6\] line 33 assertion tmp_if_expr\$\d+: SUCCESS$
7-
^\[main.assertion.7\] line 34 assertion tmp_if_expr\$\d+: SUCCESS$
8-
^\[main.assertion.8\] line 36 assertion tmp_if_expr\$\d+: SUCCESS$
9-
^\[main.assertion.9\] line 38 assertion tmp_if_expr\$\d+: SUCCESS$
10-
^\[main.assertion.10\] line 39 assertion tmp_if_expr\$\d+: SUCCESS$
6+
^\[main.assertion.6\] line 33 assertion .*: SUCCESS$
7+
^\[main.assertion.7\] line 34 assertion .*: SUCCESS$
8+
^\[main.assertion.8\] line 36 assertion .*: SUCCESS$
9+
^\[main.assertion.9\] line 38 assertion .*: SUCCESS$
10+
^\[main.assertion.10\] line 39 assertion .*: SUCCESS$
1111
^\*\* 4 of 10 failed
1212
^VERIFICATION FAILED$
1313
^EXIT=10$

regression/cbmc/Quantifiers-two-dimension-array/fixed.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ fixed.c
66
^\[main.assertion.2\] line 15 assertion a\[.*\]\[.*\] == 1: SUCCESS$
77
^\[main.assertion.3\] line 16 assertion a\[.*\]\[.*\] == 1: SUCCESS$
88
^\[main.assertion.4\] line 17 assertion a\[.*\]\[.*\] == 2: SUCCESS$
9-
^\[main.assertion.5\] line 18 assertion tmp_if_expr\$\d+: SUCCESS$
9+
^\[main.assertion.5\] line 18 assertion .*: SUCCESS$
1010
^\*\* 0 of 5 failed
1111
^VERIFICATION SUCCESSFUL$
1212
^EXIT=0$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ main.c
66
^\[main.assertion.2\] line 13 assertion a\[.*\]\[.*\] == 1: SUCCESS$
77
^\[main.assertion.3\] line 14 assertion a\[.*\]\[.*\] == 1: SUCCESS$
88
^\[main.assertion.4\] line 15 assertion a\[.*\]\[.*\] == 2: SUCCESS$
9-
^\[main.assertion.5\] line 16 assertion tmp_if_expr\$\d+: FAILURE$
9+
^\[main.assertion.5\] line 16 assertion .*: FAILURE$
1010
^\*\* 1 of 5 failed
1111
^VERIFICATION FAILED$
1212
^EXIT=10$

regression/cbmc/Quantifiers-type2/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ CORE
22
main.c
33

44
^\*\* Results:$
5-
^\[main.assertion.1\] line 12 assertion tmp_if_expr(\$\d+)?: SUCCESS$
6-
^\[main.assertion.2\] line 13 assertion tmp_if_expr\$\d+: SUCCESS$
5+
^\[main.assertion.1\] line 12 assertion b\[.*0\] == 10 && b\[.*1\] == 10: SUCCESS$
6+
^\[main.assertion.2\] line 13 assertion c\[.*0\] == 10 && c\[.*1\] == 10: SUCCESS$
77
^VERIFICATION SUCCESSFUL$
88
^EXIT=0$
99
^SIGNAL=0$

regression/contracts/assigns_validity_pointer_01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz
44
^EXIT=0$

regression/contracts/assigns_validity_pointer_04/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--enforce-contract foo --replace-call-with-contract bar --replace-call-with-contract baz _ --pointer-primitive-check
44
^EXIT=10$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--enforce-contract foo
44
^EXIT=0$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--enforce-contract foo
44
^EXIT=0$

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--enforce-contract foo
44
^EXIT=10$

0 commit comments

Comments
 (0)