- Sep 24, 2020
-
-
Marek Chalupa authored
-
- Sep 23, 2020
-
-
Marek Chalupa authored
-
- Sep 22, 2020
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We do not want to have all the stuff in one file.
-
Marek Chalupa authored
Easier to maintain.
-
Marek Chalupa authored
Do not print to stdout if not desired and make it stop after a given number of iterations (if given). Also allow to specify the starting set of paths.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
So that we can store additional information with path
-
Marek Chalupa authored
Well, not only loop headers, just on all places to which there is a DFS backedge.
-
Marek Chalupa authored
A class that visits nodes or edges in the DFS order and calls a given function on them (passes the information about node/edge and DFS edge classification).
-
- Sep 21, 2020
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
In that case, include all the error found along the path, not only those that are found in the last step of the path.
-
Marek Chalupa authored
-
Marek Chalupa authored
That is, execute the prefix of the path and then do normal fork instead of following the error edge.
-
- Sep 10, 2020
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
- Sep 04, 2020
-
-
Marek Chalupa authored
type is the 2nd argument
-
Marek Chalupa authored
So that we can use concrete domain.
-
Marek Chalupa authored
Use the core abilities of the solver.
-
Marek Chalupa authored
We do not want to make a copy of the state (and if we do, we want to further use that copy -- that was the problem in assume() method).
-
Marek Chalupa authored
That is, do not add unnecessary constraints.
-
- Sep 01, 2020
-
-
Marek Chalupa authored
Reveals a bug in handling assume statement.
-
Marek Chalupa authored
We must also add init paths when extending by more than 1 step.
-
Marek Chalupa authored
We added a wrong path to the returnlist.
-
Marek Chalupa authored
We changed the command line options
-
Marek Chalupa authored
-
Marek Chalupa authored
This argument is used only for symbolic execution.
-
Marek Chalupa authored
Oh, and rename files to match the arguments.
-
- Aug 31, 2020
-
-
Marek Chalupa authored
Check that a non-constant assumption is SAT. Without this check, we can continue executing an infeasible path which than later breaks forking as neither the condition not its negation is satisfiable.
-
- Aug 04, 2020
-
-
Marek Chalupa authored
We renamed the options.
-
Marek Chalupa authored
-
- Jul 25, 2020
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Restruture files and options for -kind.
-