Skip to content

Commit 91de164

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 e86810e commit 91de164

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
@@ -11,7 +11,8 @@ trace-values.c
1111
^ my_nested\[1.*\].f=5 .*$
1212
^ junk\$object=7 .*$
1313
^ dynamic_object1\[1.*\]=8 .*$
14-
^ my_nested\[1.*\]=\{ .f=0, .array=\{ 0, 4, 0 \} \} .*$
14+
^ my_nested\[1.*\](=\{ )?.f=0[ ,]
15+
^ my_nested\[1.*\](=\{ .f=0, )?.array=\{ 0, 4, 0 \}
1516
^VERIFICATION FAILED$
1617
--
1718
^warning: ignoring

0 commit comments

Comments
 (0)