Skip to content

Commit 277f2d0

Browse files
committed
Snapshot harness test fix
before we were extracting the value for the symbol to be used as array size, but the initialization to the extracted value is not guaranteed to happen before the initialization of the array. So we do not extract the value from the snapshot at all.
1 parent 2710fa9 commit 277f2d0

File tree

1 file changed

+1
-1
lines changed
  • regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right

1 file changed

+1
-1
lines changed

regression/snapshot-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
first,second,string_size,prefix,prefix_size --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5
3+
first,second,string_size,prefix --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 --havoc-variables prefix --size-of-array prefix:prefix_size --max-array-size 5
44
^SIGNAL=0$
55
^EXIT=0$
66
VERIFICATION SUCCESSFUL

0 commit comments

Comments
 (0)