Regression testing #6
Open
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
polgreen
force-pushed
the
regression_testing
branch
from
1fa042a to
ef31e75
Compare
polgreen
requested review from
cesaro,
kroening and
peterschrammel
as code owners
Randomized DFS shuffles the queue of successor states
Also fixes indentation and whitespace in the output function, and replaces unsigned with std::size_t, based on feedback from tautschn
Builds CFG of all program locations and computes the shortest distance from all locations in the graph to a single property. WARNING: if more than one property is given, we use the first one only. Writes these distances to the corresponding node in a locs structure passed as argument to the constructor, in order for this to be used to guide the symex search
Builds a CFG for every goto_program in goto_functions, and computes the distance for every location in the CFGs to the property, if one exists in taht CFG, or to the end of the function Writes these numbers to locst passed as argument to the constructor, in order to use numbers to guide symex search
Shortest path search heuristic computes the shortest path from all program locations to a single property. This metric is used to guide the symex search. We also introduce randomized shortest path based search, which makes a random choice when picking the next state every 1000 choices in order to avoid local minima
Computes the shortest path per function on the shortest path graph and uses this heuristic to guide the symex search
This is all the regression tests from regression/symex that only have one property, and all the regression tests from regression/symex-infeasibility that the default symex search heuristic (dfs) can complete in a reasonable amount of time.
polgreen
force-pushed
the
regression_testing
branch
from
ef31e75 to
e2daa85
Compare
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.
Adding regression tests for the shortest path search heuristic.
Note, some of these tests fail, because the master symex repository also fails those tests.