Make it possible to customise the assertions inserted for coverage instrumentation #5274
Conversation
thomasspriggs
requested review from
chrisr-diffblue,
danpoe,
hannes-steffenhagen-diffblue,
martin-cs,
peterschrammel and
smowton
as code owners
| @@ -36,18 +36,30 @@ class cover_instrumenter_baset | |||
| { | |||
| } | |||
|
|
|||
| /// The type of function used to make goto_program assertions. | |||
| using assertion_factoryt = | |||
| std::function<decltype(goto_programt::make_assertion)>; | |||
There was a problem hiding this comment.
⛏️ I'd prefer an explicit type here
There was a problem hiding this comment.
Agreed, there's no documentation here for what type signature the factory must satisfy. So if I wanted to add a new assertion factory, I'd have to reverse engineer the signature of the current one. Not a massive problem, but we should make the type explicit and document it. And as this now becomes part of the API, its an additional reason the contract needs documenting.
| @@ -36,18 +36,30 @@ class cover_instrumenter_baset | |||
| { | |||
| } | |||
|
|
|||
| /// The type of function used to make goto_program assertions. | |||
| using assertion_factoryt = | |||
| std::function<decltype(goto_programt::make_assertion)>; | |||
There was a problem hiding this comment.
Agreed, there's no documentation here for what type signature the factory must satisfy. So if I wanted to add a new assertion factory, I'd have to reverse engineer the signature of the current one. Not a massive problem, but we should make the type explicit and document it. And as this now becomes part of the API, its an additional reason the contract needs documenting.
That this change compiles shows that this member function is not specialised in any derived class. This means that we can make further changes to its signature and implementation without considering derived classes.
thomasspriggs
force-pushed
the
tas/flag_goals
branch
from
5b8a069 to
f405019
Compare
| /// The type of function used to make goto_program assertions. | ||
| using assertion_factoryt = std::function< | ||
| goto_programt::instructiont(const exprt &, const source_locationt &)>; | ||
| static_assert( |
This allows for additional logic to be added to the existing coverage instrumenters. For example instead of generating an assertion of the form `assert(guard)` we want to be able to generate an assertion of the form `assert(!in_region_of_interest || guard)`. These customised forms of instrumentation will still add assertions in the same locations and be based on top of the original expressions.
thomasspriggs
force-pushed
the
tas/flag_goals
branch
2 times, most recently
from
223329a to
443e085
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5274 +/- ##
==========================================
- Coverage 67.51% 67.5% -0.01%
==========================================
Files 1170 1170
Lines 96289 96287 -2
==========================================
- Hits 65005 65003 -2
Misses 31284 31284
Continue to review full report at Codecov.
|
This PR makes it possible to customise the assertions inserted for coverage instrumentation. We have a requirement in a downstream repository to be able to consider coverage goals only to be met when additional criteria are satisfied. The additional configure-ability this PR adds to CBMC allows us to achieve this.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/No user visible changes.My commit message includes data points confirming performance improvements (if claimed).Non claimed.