Commit 0efab54
committed
Flow-insensitive value set: don't create index expressions over non-array objects
When evaluating an index expression, the value set must ignore
pointed-to objects that are neither arrays nor vectors. Any appearance
of such objects should produce `unknown` instead. (Trying to create an
`index_exprt` with neither an array nor a vector as root object will
fail an invariant.)1 parent beb96b9 commit 0efab54
1 file changed
+5
-1
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
905 | 905 | | |
906 | 906 | | |
907 | 907 | | |
908 | | - | |
| 908 | + | |
| 909 | + | |
| 910 | + | |
| 911 | + | |
909 | 912 | | |
| 913 | + | |
910 | 914 | | |
911 | 915 | | |
912 | 916 | | |
| |||
0 commit comments