[TG-1404] Bugfix incomplete coverage in virtual method dispatch #1755
Conversation
romainbrenguier
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
|
Could you give an example of what's happening? This sounds like it should amount to the same assumption -- i.e. that we cannot possibly get to this virtual callsite. |
Yes I will try to add some regression tests to this PR
Yes the assumptions are the same. The difference is we don't generate extra blocks for this unreachable callsites. This makes a difference in the reported coverage with |
peterschrammel
changed the title
romainbrenguier
force-pushed
the
bugfix/coverage-dispatch#TG-1404
branch
2 times, most recently
from
94d7ac4 to
e1cbc33
Compare
Before block with an assume false was generated. This was leading to report of incomplete coverage. Instead of we generate assumption that the class identifier are different from the non-loaded type all in the same block.
Small variable names changes to make them more descriptive.
romainbrenguier
force-pushed
the
bugfix/coverage-dispatch#TG-1404
branch
from
e1cbc33 to
f8b5d7d
Compare
|
@mgudemann This PR and #1731 have some conflicts, so I'm not sure which one should be merged first ? |
|
@romainbrenguier is this relevant or was it obsoleted by #1830 |
|
@mgudemann #1830 fixes the bug whose effect we were trying to minimize here so the other PR is more relevant. However this change could still be made, it can remove a few instruction from the goto-programs. I just don't know if it's worth it. |
|
The main coverage issue is fixed, and this changes are no longer necessary so I'm closing this PR. |
Before this PR block with an assume false was generated.
This was leading to report of incomplete coverage.
Instead of this we generate assumption that the class identifier are
different from the non-loaded type all in the same block.