Add code_inputt and code_outputt for ID_input and ID_output
#4855
Conversation
thomasspriggs
requested review from
cesaro,
chrisr-diffblue,
cristina-david,
kroening,
martin-cs,
NathanJPhillips,
owen-mc-diffblue,
peterschrammel,
pkesseli,
smowton,
tautschnig and
thk123
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d7ee16b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/117569411
Codecov Report
@@ Coverage Diff @@
## develop #4855 +/- ##
===========================================
- Coverage 69.06% 69.06% -0.01%
===========================================
Files 1297 1294 -3
Lines 106819 106698 -121
===========================================
- Hits 73779 73688 -91
+ Misses 33040 33010 -30
Continue to review full report at Codecov.
|
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: a61789d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/117807593
|
|
||
| code_inputt::code_inputt( | ||
| const irep_idt &identifier, | ||
| exprt expression, |
There was a problem hiding this comment.
identifier usually is an index into the symbol table for us -- how about making that "description"?
There was a problem hiding this comment.
Sounds good to me, I will update this.
| std::move(location)} | ||
| { | ||
| } | ||
|
|
There was a problem hiding this comment.
It's a bit odd that you have to choose between multiple inputs in a vector with no description and one input with a description.
There was a problem hiding this comment.
The constructor which takes one input with a description is a convenient interface for use in the construction of cprover_start inside cbmc/jbmc. Its existence means that we can reduce the amount of duplication in the code which produces the various different versions of cprover_start.
The constructor which takes multiple inputs in a vector is required in order to support arbitrary calls to __CPROVER_input in user code. The definition in cprover.h is void __CPROVER_input(const char *description, ...);. This would allow the first parameter to be any pointer to char, rather than a string literal only. The ... would allow any number of expressions to be associated with the description, rather than a single expression only. The existing invariants only constrain the ... to correspond to at least one expression. Therefore this additional constructor cannot be removed without further constraining what user code is considered valid. My intention was to create a higher level internal interface, rather than make externally facing changes to existing functionality.
Is my explanation of this aspect sufficient, or do you want me to make further changes to the code in the PR - such documenting the purposes of the two constructors?
| void __CPROVER_input(const char *id, ...); | ||
| void __CPROVER_output(const char *id, ...); | ||
| void __CPROVER_input(const char *description, ...); | ||
| void __CPROVER_output(const char *description, ...); |
There was a problem hiding this comment.
A bit of a nuisance, but you'll need to add // NOLINTNEXTLINE(build/deprecated) before each of the above lines.
| /// can be added to the input code in order add instructions of this type to the | ||
| /// goto program. | ||
| /// The first argument is expected to be a C string denoting the input | ||
| /// identifier. The second argument is the expression for the input value. |
There was a problem hiding this comment.
In line with the discussion with @kroening above: I think you will need to provide this kind of documentation for each of the constructors. It's really no clear how the above maps to the two, very different constructors.
There was a problem hiding this comment.
Ah. It wasn't clear to me what change @kroening wanted. I will add doxygen for each of the constructors.
There was a problem hiding this comment.
I have added doxygen for each of the constructors.
This commit adds a higher level interface for `ID_input` based ireps. This gives us a central place to document instances of these and a central place to put the code for constructing and checking them. This makes it possible to find documentation about them and avoids duplicating the code for constructing and checking them.
This commit adds a higher level interface for `ID_output` based ireps. This gives us a central place to document instances of these and a central place to put the code for constructing and checking them. This makes it possible to find documentation about them and avoids duplicating the code for constructing and checking them.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 0617618).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/118285644
Whilst working on entry point code, I noticed the construction of
codets based onID_inputandID_outputusing direct manipulation of the.operands(). I also found an absence of documentation as to what these were. This PR adds a higher level interface and documentation for these.The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/N/A - No feature or user visible behaviour changes.