Commit 7ee921b
committed
Complete MMIO rewrites before removing unused functions
__CPROVER_mm_io_{r,w} functions are unused until rewrites via mm_io are
done, which is only done when processing the input program by CBMC.
remove_unused_functions would spuriously remove the implementation of
these function, even when they may be needed. Therefore, run mm_io
instrumentation before removing unused functions.1 parent 7162259 commit 7ee921b
File tree
2 files changed
+3
-1
lines changed- regression/cbmc/mm_io1
- src/goto-instrument
2 files changed
+3
-1
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | 3 | | |
4 | | - | |
| 4 | + | |
5 | 5 | | |
6 | 6 | | |
7 | 7 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
29 | 29 | | |
30 | 30 | | |
31 | 31 | | |
| 32 | + | |
32 | 33 | | |
33 | 34 | | |
34 | 35 | | |
| |||
899 | 900 | | |
900 | 901 | | |
901 | 902 | | |
| 903 | + | |
902 | 904 | | |
903 | 905 | | |
904 | 906 | | |
| |||
0 commit comments