Skip to content

Commit 7d61e30

Browse files
Adapt double_deref test for array cell sensitivity
Propagatiof of values of array cells lead to different expressions in VCC.
1 parent ae26270 commit 7d61e30

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
double_deref_with_pointer_arithmetic.c
33
--show-vcc
4-
^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = symex_dynamic::dynamic_object1#3\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
4+
^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
55
^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
66
^EXIT=0$
77
^SIGNAL=0$

0 commit comments

Comments
 (0)