Skip to content

Commit 26626ad

Browse files
committed
Enable previously-failing test Linking7/member-name-mismatch
Now that value-set soundly simplifies member-of-cast-of-struct, this test works as expected. This also improves the specificity of the two tests in this directory.
1 parent 650b7d4 commit 26626ad

File tree

2 files changed

+5
-3
lines changed

2 files changed

+5
-3
lines changed
Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
module2.c
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
7+
line 21 assertion \*g\.a == 42: SUCCESS
8+
line 22 assertion \*g\.c == 41: FAILURE
79
^\*\* 1 of 2 failed
810
--
911
^warning: ignoring
10-
--
11-
This is either a bug in goto-symex or value_sett (where the invariant fails).

regression/cbmc/Linking7/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,7 @@ module.c
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
^\*\* 1 of 2 failed
8+
line 21 assertion \*g\.a == 42: SUCCESS
9+
line 22 assertion \*g\.b == 41: FAILURE
810
--
911
^warning: ignoring

0 commit comments

Comments
 (0)