Skip to content

Commit ae26270

Browse files
Allow trace to assign in two steps
With field sensitivity on arrays, the element can be initialized in two steps, first the field f then the field array.
1 parent 3b374aa commit ae26270

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

regression/cbmc/trace-values/trace-values.desc

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,8 @@ trace-values.c
1212
^ null\$object=6 .*$
1313
^ junk\$object=7 .*$
1414
^ dynamic_object1\[1.*\]=8 .*$
15-
^ my_nested\[1.*\]=\{ .f=0, .array=\{ 0, 4, 0 \} \} .*$
15+
^ my_nested\[1.*\](=\{ )?.f=0[ ,]
16+
^ my_nested\[1.*\](=\{ .f=0, )?.array=\{ 0, 4, 0 \}
1617
^VERIFICATION FAILED$
1718
--
1819
^warning: ignoring

0 commit comments

Comments
 (0)