Code

Aisimplifier#173

Code

Closed

lucasccordeiro wants to merge 69 commits intodiffblue:masterdiffblue/cbmc:masterfrom

lucasccordeiro:aisimplifierlucasccordeiro/cbmc:aisimplifierCopy head branch name to clipboard

Commits

Commits on Aug 2, 2016

• support the conjunction of clauses in the assert statement

  Show description for 8242f43
  

  Lucas Cordeiro

  committed
  8242f43

  Copy full SHA for 8242f43

• implement make clean for the Makefile in the goto-analyzer regression test

  Show description for e6b00b4
  

  Lucas Cordeiro

  committed
  e6b00b4

  Copy full SHA for e6b00b4

• add additional comments related to merge and eval operations

  Show description for 21da31e
  

  Lucas Cordeiro

  committed
  21da31e

  Copy full SHA for 21da31e

• add a new test case to goto-analyzer regression suite

  Show description for a140338
  

  Lucas Cordeiro

  committed
  a140338

  Copy full SHA for a140338

• add verification options to the goto-analyzer tool

  Show description for 2476a87
  

  Lucas Cordeiro

  committed
  2476a87

  Copy full SHA for 2476a87

• add static_simplifier basic infrastructure

  Show description for e1b03de
  

  Lucas Cordeiro

  committed
  e1b03de

  Copy full SHA for e1b03de

• refactor static_analyzer

  Show description for f0d65eb
  

  Lucas Cordeiro

  committed
  f0d65eb

  Copy full SHA for f0d65eb

• simplify guards in assert, assume, and goto instructions

  Show description for 1c26254
  

  Lucas Cordeiro

  committed
  1c26254

  Copy full SHA for 1c26254

• check whether we should simplify the goto-program before showing it

  Show description for 862c181
  

  Lucas Cordeiro

  committed
  862c181

  Copy full SHA for 862c181

• add new test cases for constant propagation

  Show description for b765371
  

  Lucas Cordeiro

  committed
  b765371

  Copy full SHA for b765371

• replace constants in the goto-anlyzer

  Show description for d972859
  

  Lucas Cordeiro

  committed
  d972859

  Copy full SHA for d972859

• update test desc to the new command-line options of goto-analyzer

  Show description for f28cca3
  

  Lucas Cordeiro

  committed
  f28cca3

  Copy full SHA for f28cca3

• apply constant propagation before simplifying guards

  Show description for a19382e
  

  Lucas Cordeiro

  committed
  a19382e

  Copy full SHA for a19382e

• add new test cases related to the constant propagation

  Show description for 3e12d2c
  

  Lucas Cordeiro

  committed
  3e12d2c

  Copy full SHA for 3e12d2c

• improve support for equality in the constant propagator

  Show description for 29b327f
  

  Lucas Cordeiro

  committed
  29b327f

  Copy full SHA for 29b327f

• clean up the merge operator in the constant propagator

  Show description for 19b520a
  

  Lucas Cordeiro

  committed
  19b520a

  Copy full SHA for 19b520a

• clean up the merge operator in the constant propagator

  Show description for debcc95
  

  Lucas Cordeiro

  committed
  debcc95

  Copy full SHA for debcc95

• add test cases related to constant propagation

  Show description for 1dccbde
  

  Lucas Cordeiro

  committed
  1dccbde

  Copy full SHA for 1dccbde

• check whether the guard has been evaluated to TRUE by propagating constants

  Show description for 50c9fc1
  

  Lucas Cordeiro

  committed
  50c9fc1

  Copy full SHA for 50c9fc1

• add new test case for checking constant propagation

  Show description for c5878af
  

  Lucas Cordeiro

  committed
  c5878af

  Copy full SHA for c5878af

• update test case

  Show description for e0a1532
  

  Lucas Cordeiro

  committed
  e0a1532

  Copy full SHA for e0a1532

• do not propogate constants when dealing with loops

  Show description for a81e039
  

  Lucas Cordeiro

  committed
  a81e039

  Copy full SHA for a81e039

• remove debug flag

  Show description for 9134a60
  

  Lucas Cordeiro

  committed
  9134a60

  Copy full SHA for 9134a60

• add test cases related to constant propagation

  Show description for fdc6962
  

  Lucas Cordeiro

  committed
  fdc6962

  Copy full SHA for fdc6962

• handle ID_ge and ID_gt in the ai_analysis

  Show description for 1a0f178
  

  Lucas Cordeiro

  committed
  1a0f178

  Copy full SHA for 1a0f178

• add new test cases for constant propagation

  Show description for 44c65a6
  

  Lucas Cordeiro

  committed
  44c65a6

  Copy full SHA for 44c65a6

• improve the simplifier results

  Show description for 5da9abb
  

  Lucas Cordeiro

  committed
  5da9abb

  Copy full SHA for 5da9abb

• update test case

  Show description for f1bf538
  

  Lucas Cordeiro

  committed
  f1bf538

  Copy full SHA for f1bf538

• update test case

  Show description for 90f4d7a
  

  Lucas Cordeiro

  committed
  90f4d7a

  Copy full SHA for 90f4d7a

• fix the constant propagator merge operator

  Show description for 4edda4c
  

  Lucas Cordeiro

  committed
  4edda4c

  Copy full SHA for 4edda4c

• fix the constant propagator transform operator for goto expressions

  Show description for 1a14672
  

  Lucas Cordeiro

  committed
  1a14672

  Copy full SHA for 1a14672

• create static_verifiert class

  Show description for c071f34
  

  Lucas Cordeiro

  committed
  c071f34

  Copy full SHA for c071f34

• create static_analysert class

  Show description for c6236ea
  

  Lucas Cordeiro

  committed
  c6236ea

  Copy full SHA for c6236ea

• fix the constant propagator merge operator

  Show description for 0541104
  

  Lucas Cordeiro

  committed
  0541104

  Copy full SHA for 0541104

• add static analyser class

  Show description for 73cf9ec
  

  Lucas Cordeiro

  committed
  73cf9ec

  Copy full SHA for 73cf9ec

• fix merge operator

  Show description for 099b7ba
  

  Lucas Cordeiro

  committed
  099b7ba

  Copy full SHA for 099b7ba

• refactor constant-propagation and intervals command-line options

  Show description for ffe822d
  

  Lucas Cordeiro

  committed
  ffe822d

  Copy full SHA for ffe822d

• make sure the references are correct in the simplify_guards

  Show description for 04d03fd
  

  Lucas Cordeiro

  committed
  04d03fd

  Copy full SHA for 04d03fd

• add dump-goto option to write the simplified program

  Show description for d22cde4
  

  Lucas Cordeiro

  committed
  d22cde4

  Copy full SHA for d22cde4

• improve command-line option

  Show description for 7b6a489
  

  Lucas Cordeiro

  committed
  7b6a489

  Copy full SHA for 7b6a489

Commits on Aug 3, 2016

• remove has_assertion() check

  Show description for 697cd9f
  

  Lucas Cordeiro

  committed
  697cd9f

  Copy full SHA for 697cd9f

Commits on Aug 4, 2016

• update source_location to constant expressions

  Show description for 68c6aea
  

  Lucas Cordeiro

  committed
  68c6aea

  Copy full SHA for 68c6aea

Commits on Aug 5, 2016

• remove ID_C_cformat once we propagate the constant

  Show description for 1874066
  

  Lucas Cordeiro

  committed
  1874066

  Copy full SHA for 1874066

• remove ID_C_cformat once we propagate the constant

  Show description for b1d4414
  

  Lucas Cordeiro

  committed
  b1d4414

  Copy full SHA for b1d4414

• remove skip statements after propagating constants

  Show description for ee707af
  

  Lucas Cordeiro

  committed
  ee707af

  Copy full SHA for ee707af

• remove unreachable statements after propagating constants

  Show description for a381a39
  

  Lucas Cordeiro

  committed
  a381a39

  Copy full SHA for a381a39

Commits on Aug 8, 2016

• we do not support C/Pthreads yet

  Show description for 6e13fa7
  

  Lucas Cordeiro

  committed
  6e13fa7

  Copy full SHA for 6e13fa7

• simplify guard if it evaluates to false during constant propagation

  Show description for f388ead
  

  Lucas Cordeiro

  committed
  f388ead

  Copy full SHA for f388ead

• add a simple test case to simplify array

  Show description for 19f776d
  

  Lucas Cordeiro

  committed
  19f776d

  Copy full SHA for 19f776d

• add new test cases

  Show description for 2a055d9
  

  Lucas Cordeiro

  committed
  2a055d9

  Copy full SHA for 2a055d9

• clean up the code

  Show description for 2cffa80
  

  Lucas Cordeiro

  committed
  2cffa80

  Copy full SHA for 2cffa80

• check for expression in the interval analysis

  Show description for 8c73cd7
  

  Lucas Cordeiro

  committed
  8c73cd7

  Copy full SHA for 8c73cd7

• we have to handle symbol expression

  Show description for 93cc841
  

  Lucas Cordeiro

  committed
  93cc841

  Copy full SHA for 93cc841

Commits on Aug 10, 2016

• add initial support for propagating constants through arrays

  Show description for 6323484
  

  Lucas Cordeiro

  committed
  6323484

  Copy full SHA for 6323484

• add new test cases related to constant propagation through arrays

  Show description for 42b301c
  

  Lucas Cordeiro

  committed
  42b301c

  Copy full SHA for 42b301c

• initialise arrays in the constant propagator

  Show description for becdce5
  

  Lucas Cordeiro

  committed
  becdce5

  Copy full SHA for becdce5

• test case to check arrays initialisation in the constant propagator

  Show description for 3f227a6
  

  Lucas Cordeiro

  committed
  3f227a6

  Copy full SHA for 3f227a6

Commits on Aug 11, 2016

• add new test cases to the constant propagator

  Show description for a49821c
  

  Lucas Cordeiro

  committed
  a49821c

  Copy full SHA for a49821c

• add new test cases to the constant propagator

  Show description for 8eff586
  

  Lucas Cordeiro

  committed
  8eff586

  Copy full SHA for 8eff586

• fix merge operator

  Show description for 3845ead
  

  Lucas Cordeiro

  committed
  3845ead

  Copy full SHA for 3845ead

Commits on Aug 12, 2016

• fix merge operator

  Show description for 2b69ca0
  

  Lucas Cordeiro

  committed
  2b69ca0

  Copy full SHA for 2b69ca0

• add new test case

  Show description for 67aa621
  

  Lucas Cordeiro

  committed
  67aa621

  Copy full SHA for 67aa621

Commits on Sep 20, 2016

• write C program for debug purposes in CEGIS

  Show description for 539bfe3
  lucasccordeiro

  committed
  539bfe3

  Copy full SHA for 539bfe3

• add test case for CEGIS in control

  Show description for 4be3d20
  lucasccordeiro

  committed
  4be3d20

  Copy full SHA for 4be3d20

• write simplified C program to a file

  Show description for 87691a2
  lucasccordeiro

  committed
  87691a2

  Copy full SHA for 87691a2

• add support for simplyfing multi-threaded programs

  Show description for eed17a9
  lucasccordeiro

  committed
  eed17a9

  Copy full SHA for eed17a9

• add new test case

  Show description for eda17fa
  lucasccordeiro

  committed
  eda17fa

  Copy full SHA for eda17fa

• remove unused files

  Show description for 5396801
  lucasccordeiro

  committed
  5396801

  Copy full SHA for 5396801

• add test case constant_propagation_21

  Show description for 531f198
  lucasccordeiro

  committed
  531f198

  Copy full SHA for 531f198