[depends: #708] Adding tests that check that simplify removes statements generated by FP removal - #915

Closed

thk123 wants to merge 129 commits into

diffblue:developfrom

thk123:feature/simplify-fp-removal-tests

Commits on May 16, 2017

Make evaluation and/or simplification of conditions/expressions an ai domain operation.

Martin Brain
authored and
thk123
committed
3d59183
Implement domain_simplify for intervals.

martin
authored and
thk123
committed
1daaaed
Refactor goto-analyzer so that task, analysis, domain and output can be picked independently.

martin
authored and
thk123
committed
0060747
Remove the special case handling of --show-intervals.

Martin Brain
authored and
thk123
committed
d412b41
Implement domain_simplify for the constant domain.

Martin Brain
authored and
thk123
committed
b25bbde
Add output_json to the dependence_graph abstract domain.

martin
authored and
thk123
committed
a3875f3
Add utility function for remove_unreachable.

martin
authored and
thk123
committed
768cc67
Catch exceptions thrown in doit() in goto analyzer.

martin
authored and
thk123
committed
6153fe6
Fix merging issues in goto analyzer

danpoe
authored and
thk123
committed
62c7dd2
Fix whitespace to match coding guidelines

danpoe
authored and
thk123
committed
df7e417
Fix constant propagator

danpoe
authored and
thk123
committed
86f1731
disable two-way propagation for now

danpoe
authored and
thk123
committed
860f465
regression test changes

danpoe
authored and
thk123
committed
03045fd
Addressing goto analyzer review comments

danpoe
authored and
thk123
committed
7651ca2
option to ignore unresolved functions in the constant propagator

danpoe
authored and
thk123
committed
b20448c
use ai function output in goto-instrument

danpoe
authored and
thk123
committed
5ae66c0
more status output

danpoe
authored and
thk123
committed
250dda2
constant propagator fix

danpoe
authored and
thk123
committed
81ed6f6
add is_bottom() and is_top() to ai_domain_baset

danpoe
authored and
thk123
committed
bf78fe7
enable failed tests printer for goto-analyzer regression tests

danpoe
authored and
thk123
committed
36b72fd
enable assertions in is_threadedt

danpoe
authored and
thk123
committed
4e29ef7
fixed compilation error in debug mode

danpoe
authored and
thk123
committed
9a91f83
Check in of basic variable sensitivity framework.

thk123
authored and
thk123
committed
aae6e6e
Added constant_abstract_value implementation

thk123
authored and
thk123
committed
d7fcaff
Use variable in the constant_propogation checks

thk123
authored and
thk123
committed
cc56a35
Adding debug guarded output to the variable sensitivity domain

thk123
authored and
thk123
committed
c7c5dcf
Better stub for assigning to non-trivial symbol

thk123
authored and
thk123
committed
54f195d
Created skeleton classes for the array, pointer, struct

thk123
authored and
thk123
committed
dd98c8c
Adding a 2 element implemention of sturct abstract object

thk123
authored and
thk123
committed
e4a01df
Modifications to struct_abstract_object

thk123
authored and
thk123
committed
0d1a91a
Readded broken protected

thk123
authored and
thk123
committed
44e4f9a
Implementation of simplify

thk123
authored and
thk123
committed
6a4a4dd
Don't use static for the map as means wrong this is captured

thk123
authored and
thk123
committed
d3082d9
Added handler for logical == expression

thk123
authored and
thk123
committed
25d231f
Cleaned up the variable sensitivity framework

thk123
authored and
thk123
committed
28ef4e3
Corrected the logic for non-trivial assigns

thk123
authored and
thk123
committed
41aa910
Fixied potential dangling pointer in the struct abstract oject

thk123
authored and
thk123
committed
50aefad
Basic implementations for abstract pointer and abstract array

thk123
authored and
thk123
committed
9153942
Moved the logic for resolving logical expressions into abstract_value

thk123
authored and
thk123
committed
2f7a0fd
Fixed bug that would have occured for struct/pointer/array assigns

thk123
authored and
thk123
committed
e42e26e
Removed the requirement on two operands

thk123
authored and
thk123
committed
0fcaec4
Simplify the expression before storing

thk123
authored and
thk123
committed
2a27b35
Fixed issue where writing to a top value

thk123
authored and
thk123
committed
88a1de2
Add previously written design documentation to the relevant parts of the code.

martin
authored and
thk123
committed
d6539df
Improve the documentation of various methods.

martin
authored and
thk123
committed
c19db6f
Give a generic implementation of assume.

martin
authored and
thk123
committed
5291b75
Enable the use of assume for branches.

martin
authored and
thk123
committed
3c088e9
Basic implementation of the sensitive pointer

thk123
authored and
thk123
committed
526cd87
Fixing comments in pointer_abstract_object

thk123
authored and
thk123
committed
6707388
Adding merge state

thk123
authored and
thk123
committed
333a38f
Supporting stack when writing

thk123
authored and
thk123
committed
68c45af
Changed the pointer abstract object to store an expression

thk123
authored and
thk123
committed
f405f53
Implementing a configurable abstract object factory

Owen Jones
authored and
thk123
committed
c3c1c79
Fixed crash bug in writing to dereference of pointer to pointer

thk123
authored and
thk123
committed
9cab8ce
Improved exception message for unreasonable write

thk123
authored and
thk123
committed
6b25f9b
Checking in a demo script containg the things that currently work

thk123
authored and
thk123
committed
a133870
Added writing to pointer to demo

thk123
authored and
thk123
committed
21c2fcf
Added flags so the factory reads the flags correctly

thk123
authored and
thk123
committed
faffd81
Enable pointer sensitivity in the factory

thk123
authored and
thk123
committed
2f0e429
Added documentation to the demo script

thk123
authored and
thk123
committed
54a670c
Fixing up formatting

Owen Jones
authored and
thk123
committed
03a5516
Add simplification of the left hand side of assignments.

martin
authored and
thk123
committed
fb86f2b
Remove incorrect comment.

martin
authored and
thk123
committed
127699e
Review comments and TODOs.

martin
authored and
thk123
committed
f4d1840
Mark unreachable assertions as satisfied.

martin
authored and
thk123
committed
2938709
Document various of the key ideas behind how goto-analyze works.

martin
authored and
thk123
committed
fbd2e52
Renamed methods to provide a more consistent interface

martin
authored and
thk123
committed
b8aa460
Protect top and bottom as much as possible.

martin
authored and
thk123
committed
a191670
Output should be const-clean.

martin
authored and
thk123
committed
714a9f7
Implementing sensitive struct abstract object

danpoe
authored and
thk123
committed
9c33e9a
If anything is assigned the value bottom, the whole domain should be set to bottom.

martin
authored and
thk123
committed
8e44147
A missing case in the factory code means that constant assertions were not being

martin
authored and
thk123
committed
754f418
Fix overwrite for CLONE and MERGE

Owen Jones
authored and
thk123
committed
5f2407c
In abstract objects the state should be private and merge_state protected.

martin
authored and
thk123
committed
8f8af13
Enforced const interface for abstract objects

martin
authored and
thk123
committed
9c1a3a5
Fix crash

Owen Jones
authored and
thk123
committed
7e7218a
Minimal reproducer for struct problem

Owen Jones
authored and
thk123
committed
9c272cc
Use the correct abstract object when performing a transform
thk123
committed
723ae80
Corrected merge action in the abstract enviroment
thk123
committed
fae976d
Correct struct write for unknown component
thk123
committed
c8e3d7d
Correcting type check in struct abstract object
thk123
committed
e047346
Fix for crash

Owen Jones
authored and
thk123
committed
f9a3cbb
Basic implementation of the constant_array_abstract_object
thk123
committed
1d57f80
Array initialization now works with the abstract object
thk123
committed
4aef235
Added merge_state to constant_array_abstract_object
thk123
committed
2fc020d
Adding function header comments
thk123
committed
d944c92
Removed unnecessary copies
thk123
committed
514c92c
Updating the demo script
thk123
committed
07cd3b3
Adding output function to struct
thk123
committed
77bbcb0
Made verify stricter
thk123
committed
9b8655a
Fixed bug where top wasn't being cleared
thk123
committed
ed1dfce
Bug fixes for the array abstract object
thk123
committed
34ce529
Corrected and simplified constructor for the pointer abstract object
thk123
committed
d3de879
Corrected implementation of flow sensitivity
thk123
committed
9cd204a
Tidy up includes
thk123
committed
1d4c393
Correcting implemenations of the write methods for pointer and struct
thk123
committed
fa17c4e
Refactor the ai_simplify into a lhs function
thk123
committed
776b24f
Corrected constructing object for failed evaluation
thk123
committed
2628f99
Fixing constant propogation test
thk123
committed
8818f01
Linting fixes
thk123
committed
fae0baa
Modified lambda to compile under Windows compiler.
thk123
committed
2b49093
Improved the removing top elements in map merge
thk123
committed
9211406
Modified code to not crash when writing to an pointer arithmetic on lhs
thk123
committed
25bb2e5
Adding tests for reading and writing to/from ararys through points
thk123
committed
ba4b2f2
Fixed bug when doing a merge write to a pointer
thk123
committed
f233cec
Reworked the double dispatch of the merge
thk123
committed
65e4dd1
Removing default copy constructors
thk123
committed
12433b8
Replacing map based switch statments with chained if/elses
thk123
committed
f8a1f01
Explained why top must be used as the else clause in eval
thk123
committed
3fa2bf4
Don't make copies unnecessarily when merging
thk123
committed
8118bef
Using enable_shared_from_this to eliminate naked pointers
thk123
committed
4c761d2
Adding unit tests for merging of abstract objects
thk123
committed
009de7e
Fixed bugs revealed by unit tests
thk123
committed
6c8cfbb
Adding unit tests for constant abstract object.
thk123
committed
a6fdf8f
Adding tests for constant array
thk123
committed
760cbd8
Adding unit tests for the struct abstract object
thk123
committed
c0fcd70
Corrected merge methods for pointer and struct
thk123
committed
d5d3466
Rewriting the constant_abstract_value::merge using behaviour driven design
thk123
committed
7788d11
Replaced assert with __CPROVER_assert
thk123
committed
3cb9ebd
Use Behaviour Driven Design testing for abstract object merge
thk123
committed
28481c9
Struct and array AO unit tests using behaviour driven design
thk123
committed
7c8912c
Corrected guard on specialised merge
thk123
committed
9ff56b0
Made pointer to array name consistent
thk123
committed
67da5aa
Constant array reading from top handled correctly
thk123
committed
d10989e
Completed test suite for full struct and constant array AOs
thk123
committed
2f56609
Correctly set up the enviroment before running tests
thk123
committed
c1736c4
Extracted out logic for when to use a 2 value merge
thk123
committed
92a84dc
Adding tests for simplify function pointer removal
thk123
committed
79a8b9f
Simplify fp tests now checking the simplified GOTO
thk123
committed
211cd21

Uh oh!

Commits

Commits on May 16, 2017