Symex improvements #151
Merged
Symex improvements #151
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tautschnig
force-pushed
the
symex-improvements
branch
from
aa3a00d to
1499340
Compare
|
Hi Michael, thanks for this - greatly appreciated. Which examples have you been testing this on? |
|
@DanielNeville Apologies for the late response. I can't share the code this being run on I'm afraid - but I'd be happy to give any code (that can be shared) a try and debug&profile further. |
tautschnig
force-pushed
the
symex-improvements
branch
from
1499340 to
2f2dd76
Compare
tautschnig
force-pushed
the
symex-improvements
branch
from
2f2dd76 to
b806a2f
Compare
tautschnig
force-pushed
the
symex-improvements
branch
from
b806a2f to
e1bbc52
Compare
tautschnig
force-pushed
the
symex-improvements
branch
2 times, most recently
from
1113dac to
c80d192
Compare
|
@tautschnig can you rebase, please? |
tautschnig
force-pushed
the
symex-improvements
branch
2 times, most recently
from
813b908 to
dac4764
Compare
|
Rebase done. |
tautschnig
force-pushed
the
symex-improvements
branch
from
dac4764 to
a0b01b5
Compare
tautschnig
force-pushed
the
symex-improvements
branch
from
a0b01b5 to
b168360
Compare
tautschnig
force-pushed
the
symex-improvements
branch
from
b168360 to
0297e02
Compare
tautschnig
force-pushed
the
symex-improvements
branch
4 times, most recently
from
3e37614 to
6a5b33c
Compare
|
My concern about this is that we can no longer have limit "0", e.g., "no interleaving". |
vectors don't need to be handled, they have been removed via remove_vector.
Unlike CBMC, all output is enabled in debug mode only.
All symex limits use value -1 as marking "not set". Use size_t for counting statistics.
|
The defaults for limits are now set to -1, and 0 has become a valid limit. |
tautschnig
force-pushed
the
symex-improvements
branch
from
6a5b33c to
73adfb0
Compare
|
Ah, now produces warnings because of signed/unsigned comparisons. The is_set idiom may have its advantages. |
smowton
pushed a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
Bugfixes in the Evalautor of our benchmarks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Major performance improvement (taking one of my examples from 13s to 0.3s) when dealing with larger static arrays via c6a92a8; the other patches are mostly cleanup and some improvements to output. Finally a new option to perform time-limited search (aa3a00d).