Commit fffc77e
committed
Location coverage reporting should ignore globals
We iterate over instructions in non-built-in functions, and it is
therefore reasonable to expect that all source locations have functions
that they belong to. If symbols declared at global scope are part of
expressions then this shouldn't yield calling them out in location
coverage. (That's just where they were declared, it doesn't even
strictly imply their assignments were covered.)
Fixes: #69781 parent 8bf2503 commit fffc77e
File tree
3 files changed
+30
-2
lines changed- regression/cbmc-cover/location2
- src/goto-instrument
3 files changed
+30
-2
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
163 | 163 | | |
164 | 164 | | |
165 | 165 | | |
166 | | - | |
167 | | - | |
| 166 | + | |
| 167 | + | |
| 168 | + | |
| 169 | + | |
| 170 | + | |
168 | 171 | | |
169 | 172 | | |
170 | 173 | | |
| |||
0 commit comments