Unified wrapper script for CPROVER tools #4
Conversation
tautschnig
left a comment
tautschnig
left a comment
There was a problem hiding this comment.
I've implementation suggestions via 2 extra commits, which should be squashed. Let me know what you think about my comments.
2ls.inc
Outdated
| OPTIONS["termination"]="--termination --competition-mode" | ||
| OPTIONS["overflow"]="--k-induction --signed-overflow-check --competition-mode" | ||
| OPTIONS["memsafety"]="--k-induction --pointer-check --memory-leak-check --bound\ | ||
| s-check --competition-mode" |
There was a problem hiding this comment.
May I suggest to break this line at a whitespace?
For all of these: would it be bad idea to move --k-induction --competiton-mode into the run() function, at which point CBMC and 2LS would be using the same OPTIONS? Thus the entire OPTIONS declaration could be moved into the common file, and values could be overwritten when necessary?
There was a problem hiding this comment.
That's possible if $PROP is available in the the run() function so that I can distinguish between safety and termination.
2ls.inc
Outdated
| run() | ||
| { | ||
| $TOOL_BINARY --graphml-witness $LOG.witness $BIT_WIDTH $PROPERTY --function $\ | ||
| ENTRY $BM >> $LOG.ok 2>&1 |
There was a problem hiding this comment.
Again, I would suggest to break the line at a whitespace.
Run the Makefile to build the tool wrapper script from tool-wrapper.inc and tool-specific includes which define tool and executable names as well as a run function, currently provided for CBMC and 2LS. tool-wrapper.inc contains a mapping from SV-COMP properties to the CPROVER property instrumentation options.
peterschrammel
force-pushed
the
unified-script
branch
from
8b39b01 to
5e479a5
Compare
|
@tautschnig, I have squashed your Makefile improvements and moved the options block into the common wrapper script. |
2 participants
The Makefile now builds the tool wrapper script from tool-wrapper.inc
and tool-specific includes which define tool and executable names
as well as mappings from properties to tool options,
currently provided for CBMC and 2LS.