Skip to content

Commit 5b30b06

Browse files
committed
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: #2925
1 parent 5914d75 commit 5b30b06

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)