Skip to content

Commit 544a4aa

Browse files
tautschnigjezhiggins
authored andcommitted
Memcpy for pointers involving structs was fixed via field sensitivity
This test passes as of ca9fcb7, except for the missing "line NN" part that wasn't included in the pattern to be matched. Fixes: diffblue#2925
1 parent 3d970fe commit 544a4aa

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

regression/cbmc-library/memcpy-01/test.desc

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
--bounds-check --pointer-check
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
7-
^\[main\.assertion\.5\] assertion q\.s->x == 42: SUCCESS$
8-
^\[main\.assertion\.6\] assertion q\.s->y == 43: SUCCESS$
7+
^\[main\.assertion\.5\] line 46 assertion q\.s->x == 42: SUCCESS$
8+
^\[main\.assertion\.6\] line 47 assertion q\.s->y == 43: SUCCESS$
99
--
1010
^warning: ignoring
1111
--

0 commit comments

Comments
 (0)