Commit a353fbb
committed
Simplification of pointer comparison: do not assume numeric types
As we cannot (or chose not to) catch all type inconsistencies in the
language front-end, we may pass expressions to simplification that do
not adhere to typing expectations. The included example is such a case,
where the missing declaration of `memcpy` makes the struct-to-pointer
cast get all the way to the middle end.
Test is based on a sample generated by C-Reduce when starting from an
SV-COMP task.1 parent 95097a8 commit a353fbb
File tree
3 files changed
+36
-5
lines changed- regression/cbmc-library/memcpy-06
- src/util
3 files changed
+36
-5
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1645 | 1645 | | |
1646 | 1646 | | |
1647 | 1647 | | |
1648 | | - | |
1649 | | - | |
1650 | | - | |
1651 | | - | |
| 1648 | + | |
1652 | 1649 | | |
| 1650 | + | |
| 1651 | + | |
| 1652 | + | |
| 1653 | + | |
| 1654 | + | |
| 1655 | + | |
| 1656 | + | |
| 1657 | + | |
| 1658 | + | |
1653 | 1659 | | |
1654 | 1660 | | |
1655 | | - | |
1656 | 1661 | | |
1657 | 1662 | | |
1658 | 1663 | | |
| |||
0 commit comments