Commit 115b214
committed
Pointer flattening: convert typecast through cache
This is to make sure we do not convert the same expression twice, which
would result in fresh variables for accesses into unbounded arrays,
resulting in spurious verification failures.
This was observed with --paths lifo on Pointer_array6 once alignment
assumptions in value-set dereferencing are fixed.1 parent b08632a commit 115b214
1 file changed
+1
-1
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
732 | 732 | | |
733 | 733 | | |
734 | 734 | | |
735 | | - | |
| 735 | + | |
736 | 736 | | |
737 | 737 | | |
738 | 738 | | |
| |||
0 commit comments