Add back two declarations needed for test-gen #4328
Conversation
These were removed in diffblue#4216. This is temporary and these two declarations will be removed once https://github.com/diffblue/test-gen/tree/svorenova/goto-checker is merged.
allredj
requested review from
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
| @@ -193,6 +193,10 @@ class bmct:public safety_checkert | |||
|
|
|||
| friend class bmc_all_propertiest; | |||
|
|
|||
| // \todo remove these two declarations once test-gen dependency is fixed | |||
| bool cover(const goto_functionst &goto_functions); | |||
There was a problem hiding this comment.
How does adding the declaration (but not a definition) make a difference?
There was a problem hiding this comment.
Heh... wondered the same thing - I think the answer is we provide the definition in the test-gen repo. I vaguely remember some dark magic where we linked a different bmc_cover.cpp because it had diverged too much on the old branch...
| @@ -193,6 +193,10 @@ class bmct:public safety_checkert | |||
|
|
|||
| friend class bmc_all_propertiest; | |||
|
|
|||
| // \todo remove these two declarations once test-gen dependency is fixed | |||
| bool cover(const goto_functionst &goto_functions); | |||
There was a problem hiding this comment.
❓ How does adding a declaration without definition help? Because TG provides a implementation.
There was a problem hiding this comment.
But ... this isn't declared virtual?
There was a problem hiding this comment.
No - TG compiles and links a copy of bmc_cover.cpp with the bmct::cover directly.
There was a problem hiding this comment.
I see - so it's technical debt coming to haunt you 👻
|
Bump is here: https://github.com/diffblue/test-gen/pull/3122 |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: bb64e19).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103192554
|
This won't work after all. |
These were removed in #4216.
This is temporary and these two declarations will be removed once https://github.com/diffblue/test-gen/tree/svorenova/goto-checker is merged (PR currently being prepared).