Allow to force-load symbols from the cprover library #6844
Conversation
remi-delmas-3000
added
blocker
aws
remi-delmas-3000
requested review from
chris-ryder,
kroening and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #6844 +/- ##
===========================================
+ Coverage 77.04% 77.79% +0.74%
===========================================
Files 1594 1567 -27
Lines 185287 179719 -5568
===========================================
- Hits 142763 139804 -2959
+ Misses 42524 39915 -2609
Continue to review full report at Codecov.
|
src/ansi-c/cprover_library.cpp
Outdated
| std::string library_text; | ||
|
|
||
| library_text=get_cprover_library_text(functions, symbol_table); | ||
| library_text = get_cprover_library_text(functions, symbol_table, false); |
There was a problem hiding this comment.
While at it: I don't see why declaration and definition should be separate instructions here, can you please merge them?
src/ansi-c/cprover_library.cpp
Outdated
| std::string library_text; | ||
| library_text = get_cprover_library_text(functions, symbol_table, true); |
There was a problem hiding this comment.
As above: these should not be two instructions.
| special.insert("__delete"); | ||
| special.insert("__delete_array"); | ||
| // plus any extra symbols we wish to keep | ||
| if(!keep.empty()) |
There was a problem hiding this comment.
I don't think that test even is necessary for .empty() is the same as .begin() == .end().
TGWDB
left a comment
TGWDB
left a comment
There was a problem hiding this comment.
Please include some tests.
To have additional tests over the existing ones it will be necessary to add new functionality. That is being built, and is the reason for this PR in the first place. But it will also mean that this PR will become significantly larger. |
|
Hi, @TGWDB testing this is not possible from the ansi-C front end, so it would require to write C++ unit tests. I took great care in ensuring no change in behaviour for all preexisting functions which do not have this extra 'keep' argument. Since this new force-loading feature is meant to support new features in function contract instrumentation, which will themselves be testable from the C front-end, I expect code coverage to be achieved when this new contract instrumentation ships (hopefully before the end of May). Would you be OK with the following: merge this PR, and simultaneously open a ticket to remind us to check for coverage when the next related PR gets merged ? Alternatively, I could keep this PR's commits in the history of the next contract-feature PR, but since it is going to be quite substantial, I'd rather have this PR kept separate. Tell me what you think ! |
not already found in the symbol table and ensure they survive `remove_internal_symbols`.
remi-delmas-3000
force-pushed
the
force-load-cprover-library
branch
from
7967f25 to
3411b22
Compare
Thanks for the explanation. I'm going to approve this and look for tests in future. |
3 participants
The existing behaviour of
cprover_c_library_factoryis to load functions only if they already occur in the symbol table. This makes it impossible to load a library function unless a header declaring this function was included in the user's program and the function was actually used in the program.This patch makes it possible to load functions of the cprover library even if they not already found in the symbol table and makes sure they survive the
remove_internal_symbolscleanup pass.The use case for this is to be able to programatically load functions in the symbol table before generating code that uses these functions as part of function contracts instrumentation.