[depends: #472] Variable Sensitivity Domain#708

Closed

thk123 wants to merge 129 commits intodiffblue:developfrom

thk123:feature/variable-sensitivity-domain

Commits on Jun 15, 2017

Fix constant propagator.
martin
committed
disable two-way propagation for now

danpoe
authored and
martin
committed
Addressing constant domain review comments by Daniel Poetzl.
martin
committed
constant propagator fix

danpoe
authored and
martin
committed
Add is_bottom() and is_top() to ai_domain_baset and derived domains.
martin
committed
Use is_bottom() to catch unreachable functions.
martin
committed
Refactor goto-analyzer so that task, analysis, domain and output can be picked independently.
martin
committed
Remove the special case handling of --show-intervals.

Martin Brain
authored and
martin
committed
Add support for dependency graph display.
martin
committed
Program simplification now removes unused instructions.
martin
committed
Catch exceptions thrown in doit() in goto analyzer.
martin
committed
Fix merging issues in goto analyzer.
martin
committed
Fix whitespace to match coding guidelines

danpoe
authored and
martin
committed
Whitespace fixes in goto-analyzer.
martin
committed
regression test changes

danpoe
authored and
martin
committed
Addressing goto analyzer review comments by Daniel Poetzl.
martin
committed
option to ignore unresolved functions in the constant propagator

danpoe
authored and
martin
committed
Test that requires is_bottom() and is_top().
martin
committed
Improve status output.
martin
committed
enable failed tests printer for goto-analyzer regression tests

danpoe
authored and
martin
committed
enable assertions in is_threadedt

danpoe
authored and
martin
committed
Update the use of ai_simplify for the introduction of ai_simplify_lhs.
martin
committed
Check in of basic variable sensitivity framework.

thk123
authored and
thk123
committed
Added constant_abstract_value implementation

thk123
authored and
thk123
committed
Use variable in the constant_propogation checks

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

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

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

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

thk123
authored and
thk123
committed
Modifications to struct_abstract_object

thk123
authored and
thk123
committed
Readded broken protected

thk123
authored and
thk123
committed
Implementation of simplify

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

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

thk123
authored and
thk123
committed
Cleaned up the variable sensitivity framework

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

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

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

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

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

thk123
authored and
thk123
committed
Removed the requirement on two operands

thk123
authored and
thk123
committed
Simplify the expression before storing

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

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

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

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

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

martin
authored and
thk123
committed
Basic implementation of the sensitive pointer

thk123
authored and
thk123
committed
Fixing comments in pointer_abstract_object

thk123
authored and
thk123
committed
Adding merge state

thk123
authored and
thk123
committed
Supporting stack when writing

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

thk123
authored and
thk123
committed
Implementing a configurable abstract object factory

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

thk123
authored and
thk123
committed
Improved exception message for unreasonable write

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

thk123
authored and
thk123
committed
Added writing to pointer to demo

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

thk123
authored and
thk123
committed
Enable pointer sensitivity in the factory

thk123
authored and
thk123
committed
Added documentation to the demo script

thk123
authored and
thk123
committed
Fixing up formatting

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

martin
authored and
thk123
committed
Remove incorrect comment.

martin
authored and
thk123
committed
Review comments and TODOs.

martin
authored and
thk123
committed
Mark unreachable assertions as satisfied.

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

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

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

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

martin
authored and
thk123
committed
Implementing sensitive struct abstract object

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

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

martin
authored and
thk123
committed
Fix overwrite for CLONE and MERGE

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

martin
authored and
thk123
committed
Enforced const interface for abstract objects

martin
authored and
thk123
committed
Fix crash

Owen Jones
authored and
thk123
committed
Minimal reproducer for struct problem

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

Owen Jones
authored and
thk123
committed
Basic implementation of the constant_array_abstract_object
thk123
committed
Array initialization now works with the abstract object
thk123
committed
Added merge_state to constant_array_abstract_object
thk123
committed
Adding function header comments
thk123
committed
Removed unnecessary copies
thk123
committed
Updating the demo script
thk123
committed
Adding output function to struct
thk123
committed
Made verify stricter
thk123
committed
Fixed bug where top wasn't being cleared
thk123
committed
Bug fixes for the array abstract object
thk123
committed
Corrected and simplified constructor for the pointer abstract object
thk123
committed
Corrected implementation of flow sensitivity
thk123
committed
Tidy up includes
thk123
committed
Correcting implemenations of the write methods for pointer and struct
thk123
committed
Refactor the ai_simplify into a lhs function
thk123
committed
Corrected constructing object for failed evaluation
thk123
committed
Fixing constant propogation test
thk123
committed
Linting fixes
thk123
committed
Modified lambda to compile under Windows compiler.
thk123
committed
Improved the removing top elements in map merge
thk123
committed
Modified code to not crash when writing to an pointer arithmetic on lhs
thk123
committed
Adding tests for reading and writing to/from ararys through points
thk123
committed
Fixed bug when doing a merge write to a pointer
thk123
committed
Reworked the double dispatch of the merge
thk123
committed
Removing default copy constructors
thk123
committed
Replacing map based switch statments with chained if/elses
thk123
committed
Explained why top must be used as the else clause in eval
thk123
committed
Don't make copies unnecessarily when merging
thk123
committed
Using enable_shared_from_this to eliminate naked pointers
thk123
committed
Adding unit tests for merging of abstract objects
thk123
committed
Fixed bugs revealed by unit tests
thk123
committed
Adding unit tests for constant abstract object.
thk123
committed
Adding tests for constant array
thk123
committed
Adding unit tests for the struct abstract object
thk123
committed
Corrected merge methods for pointer and struct
thk123
committed
Rewriting the constant_abstract_value::merge using behaviour driven design
thk123
committed
Replaced assert with __CPROVER_assert
thk123
committed
Use Behaviour Driven Design testing for abstract object merge
thk123
committed
Struct and array AO unit tests using behaviour driven design
thk123
committed
Corrected guard on specialised merge
thk123
committed
Made pointer to array name consistent
thk123
committed
Constant array reading from top handled correctly
thk123
committed
Completed test suite for full struct and constant array AOs
thk123
committed
Correctly set up the enviroment before running tests
thk123
committed
Extracted out logic for when to use a 2 value merge
thk123
committed
Improved comment in the LHS simplify
thk123
committed
Fixed ai_simplify in variable sensitivity domain to use new interface
thk123
committed

[depends: #472] Variable Sensitivity Domain#708thk123 wants to merge 129 commits intodiffblue:developdiffblue/cbmc:developfrom thk123:feature/variable-sensitivity-domainthk123/cbmc:feature/variable-sensitivity-domainCopy head branch name to clipboard

Commits

Commits on Jun 15, 2017

[depends: #472] Variable Sensitivity Domain#708
thk123 wants to merge 129 commits intodiffblue:developfrom
thk123:feature/variable-sensitivity-domain