Commit 003b7c7
committed
Field sensitivity: also rewrite byte extract to type casts
With model-checking/kani#2456 we see examples
where a pointer of a different type is byte-extracted from a union. This
is caused by Rust's niche placement. `get_subexpression_at_offset`
already catered for that, but we didn't use it in field expansion.1 parent 453eb65 commit 003b7c7
File tree
2 files changed
+23
-0
lines changed- regression/contracts/assigns_enforce_conditional_unions
- src/goto-symex
2 files changed
+23
-0
lines changedLines changed: 9 additions & 0 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
123 | 123 | | |
124 | 124 | | |
125 | 125 | | |
| 126 | + | |
| 127 | + | |
| 128 | + | |
| 129 | + | |
| 130 | + | |
| 131 | + | |
| 132 | + | |
| 133 | + | |
| 134 | + | |
| 135 | + | |
| 136 | + | |
| 137 | + | |
| 138 | + | |
| 139 | + | |
126 | 140 | | |
127 | 141 | | |
128 | 142 | | |
| |||
0 commit comments