Code

New goto-analyzer infrastructure#264

Code

Closed

martin-cs wants to merge 24 commits intodiffblue:masterdiffblue/cbmc:masterfrom

martin-cs:goto-analyzermartin-cs/cbmc:goto-analyzerCopy head branch name to clipboard

Commits

Commits on Nov 1, 2016

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

  

  Martin Brain

  authored and

  martin

  committed
  51eb520

  Copy full SHA for 51eb520

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

  

  Martin Brain

  authored and

  martin

  committed
  b4aaab5

  Copy full SHA for b4aaab5

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

  

  Martin Brain

  authored and

  martin

  committed
  1283be2

  Copy full SHA for 1283be2

• Fixes for the previous commit.

  

  Martin Brain

  authored and

  martin

  committed
  9fe825b

  Copy full SHA for 9fe825b

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

  

  Martin Brain

  authored and

  martin

  committed
  6f4ce96

  Copy full SHA for 6f4ce96

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

  

  Martin Brain

  authored and

  martin

  committed
  92bd719

  Copy full SHA for 92bd719

• Lucas' rather fantastic regression tests.

  

  Martin Brain

  authored and

  martin

  committed
  9371ffc

  Copy full SHA for 9371ffc

• Make the help text more consistent.

  

  Martin Brain

  authored and

  martin

  committed
  76cb0eb

  Copy full SHA for 76cb0eb

• Add a missing flag.

  

  Martin Brain

  authored and

  martin

  committed
  0b8e479

  Copy full SHA for 0b8e479

• Update the flags used to match the refactoring.

  

  Martin Brain

  authored and

  martin

  committed
  c018a31

  Copy full SHA for c018a31

• Correct the statistics printed by the simplifier.

  

  Martin Brain

  authored and

  martin

  committed
  d087058

  Copy full SHA for d087058

• ... and again ...

  

  Martin Brain

  authored and

  martin

  committed
  2c4fede

  Copy full SHA for 2c4fede

• Improve the simplification of the constant domain.

  

  Martin Brain

  authored and

  martin

  committed
  b88e678

  Copy full SHA for b88e678

• Simplify arguments to function calls.

  

  Martin Brain

  authored and

  martin

  committed
  5792ff1

  Copy full SHA for 5792ff1

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

  

  martin

  committed
  1fa7691

  Copy full SHA for 1fa7691

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

  

  martin

  committed
  273d23e

  Copy full SHA for 273d23e

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

  

  martin

  committed
  0a5d365

  Copy full SHA for 0a5d365

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

  

  martin

  committed
  a7be3a6

  Copy full SHA for a7be3a6

• Fix an ambiguity in method overloading.

  

  martin

  committed
  5ff9c51

  Copy full SHA for 5ff9c51

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

  

  martin

  committed
  0ca3ece

  Copy full SHA for 0ca3ece

• Add output_json to the dependence_graph abstract domain.

  

  martin

  committed
  dee1f4b

  Copy full SHA for dee1f4b

• ... and the header file ...

  

  martin

  committed
  8cddfbb

  Copy full SHA for 8cddfbb

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

  

  martin

  committed
  d44063a

  Copy full SHA for d44063a

• Dot output needs to be in a graph.

  

  martin

  committed
  15e3e3c

  Copy full SHA for 15e3e3c