New goto-analyzer infrastructure : take 2#315

Closed

martin-cs wants to merge 32 commits intodiffblue:masterfrom

martin-cs:goto-analyzer-2

Commits on Nov 17, 2016

Add XML and JSON output to the base of both domains and analysis.

Martin Brain
authored and
martin
committed
Make evaluation and/or simplification of conditions a domain operation.

Martin Brain
authored and
martin
committed
Refactor goto-analyze so that task, analysis, domain and output can all be selected independently.

Martin Brain
authored and
martin
committed
Fixes for the previous commit.

Martin Brain
authored and
martin
committed
Remove the special case handling of --show-intervals. --show --intervals does more and --show-intervals now invokes it.

Martin Brain
authored and
martin
committed
Lucas' improvements and fixes to the constant and interval domains.

Martin Brain
authored and
martin
committed
Lucas' rather fantastic regression tests.

Martin Brain
authored and
martin
committed
Make the help text more consistent.

Martin Brain
authored and
martin
committed
Add a missing flag.

Martin Brain
authored and
martin
committed
Update the flags used to match the refactoring.

Martin Brain
authored and
martin
committed
Correct the statistics printed by the simplifier.

Martin Brain
authored and
martin
committed
... and again ...

Martin Brain
authored and
martin
committed
Improve the simplification of the constant domain.

Martin Brain
authored and
martin
committed
Simplify arguments to function calls.

Martin Brain
authored and
martin
committed
s/sequential/flow-sensitive/ as there are other sequential analyses.
martin
committed
Add an extra argument to domain_simplify so that the left hand side of assignment operations is treated differently.
martin
committed
Add a caveat that failures are only assertion failures if they are reachable.
martin
committed
Update and check the test cases. FUTURE for things where precision is currently insufficient.
martin
committed
Fix an ambiguity in method overloading.
martin
committed
Improve error reporting for unsupported combinations of task / interpreter / domain.
martin
committed
Add output_json to the dependence_graph abstract domain.
martin
committed
... and the header file ...
martin
committed
Add support for generating the dependency graph to goto-analyze, including dot format.
martin
committed
Dot output needs to be in a graph.
martin
committed
Fix a travis build failure.
martin
committed
Finish fixing the travis issue.
martin
committed
Improve handling of exceptions.
martin
committed
Implement feature request for simpler JSON output.
martin
committed
Add support for reachability slicing after simplification; disabled for now.
martin
committed
Add a utility function for removing unreachable instructions from all goto_programs.
martin
committed
An alternative approach to slicing unreachable instructions.
martin
committed
Consistent capitalisation of status messages.
martin
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New goto-analyzer infrastructure : take 2#315

Commits on Nov 17, 2016

Add XML and JSON output to the base of both domains and analysis.

Make evaluation and/or simplification of conditions a domain operation.

Refactor goto-analyze so that task, analysis, domain and output can all be selected independently.

Fixes for the previous commit.

Remove the special case handling of --show-intervals. --show --intervals does more and --show-intervals now invokes it.

Lucas' improvements and fixes to the constant and interval domains.

Lucas' rather fantastic regression tests.

Make the help text more consistent.

Add a missing flag.

Update the flags used to match the refactoring.

Correct the statistics printed by the simplifier.

... and again ...

Improve the simplification of the constant domain.

Simplify arguments to function calls.

s/sequential/flow-sensitive/ as there are other sequential analyses.

Add an extra argument to domain_simplify so that the left hand side of assignment operations is treated differently.

Add a caveat that failures are only assertion failures if they are reachable.

Update and check the test cases. FUTURE for things where precision is currently insufficient.

Fix an ambiguity in method overloading.

Improve error reporting for unsupported combinations of task / interpreter / domain.

Add output_json to the dependence_graph abstract domain.

... and the header file ...

Add support for generating the dependency graph to goto-analyze, including dot format.

Dot output needs to be in a graph.

Fix a travis build failure.

Finish fixing the travis issue.

Improve handling of exceptions.

Implement feature request for simpler JSON output.

Add support for reachability slicing after simplification; disabled for now.

Add a utility function for removing unreachable instructions from all goto_programs.

An alternative approach to slicing unreachable instructions.

Consistent capitalisation of status messages.