Disjunctive domains#13

Open

wadkhlemshem wants to merge 329 commits intopeterschrammel:masterfrom

wadkhlemshem:disjunctive-domains

This pull request is big! We're only showing the most recent 250 commits

Commits on Nov 6, 2017

Comment unknown objects equalities - causing problems

viktormalik
authored and
peterschrammel
committed
Heap-interval domain: combination of domains.

viktormalik
authored and
peterschrammel
committed
Heap-interval domain: remove abstract value from the domain (it is not used).

viktormalik
authored and
peterschrammel
committed
Heap domain: include all pointers into the pointer part of the template.

viktormalik
authored and
peterschrammel
committed
SSA heap analysis: use only with interprocedural heap analysis.

viktormalik
authored and
peterschrammel
committed
Change heap regression tests.

viktormalik
authored and
peterschrammel
committed
Comments and cleanup for heap branch.

viktormalik
authored and
peterschrammel
committed
Update heap tests.

viktormalik
authored and
peterschrammel
committed
Fix errors overlooked in merge of heap branch.

viktormalik
authored and
peterschrammel
committed
Changes needed for the merge of heap branch into master.

viktormalik
authored and
peterschrammel
committed
Improved formatting.

viktormalik
authored and
peterschrammel
committed
Fix in ssa_inliner: use utility function for obtaining identifier of pointer object.

viktormalik
authored and
peterschrammel
committed
Repair code formatting for heap branch so that cpplint succeedes.

viktormalik
authored and
peterschrammel
committed
Strategy solver for heap domain does not fail when the solver returns address of something different than a symbol.

viktormalik
authored and
peterschrammel
committed
Fix bugs in heap-interval domain combination.

viktormalik
authored and
peterschrammel
committed
Abort if tests fail
peterschrammel
committed
Fix formatting
peterschrammel
committed
Set termination/global2 and interprocedural/contextsensitive to KNOWNBUG
peterschrammel
committed
version 0.5.3
peterschrammel
committed
Fix compiler warning
peterschrammel
committed
Fix nontermination witnesses
peterschrammel
committed
Remove old nontermination witnesses
peterschrammel
committed
Update CBMC pointer
peterschrammel
committed
Better nontermination property ids
peterschrammel
committed

Commits on Nov 12, 2017

Commits on Nov 14, 2017

Output correctness witness for termination
peterschrammel
committed

Commits on Nov 18, 2017

Commits on Nov 19, 2017

More heap tests
peterschrammel
committed
Fix can_convert_ssa_expr
peterschrammel
committed
Improve debug output
peterschrammel
committed
Fix show_ssa for ssa_heap_analysis
peterschrammel
committed
Heap analysis: use symbolic dereferencing when accessing objects in the heap.

viktormalik
authored and
peterschrammel
committed
Fix bug in dereference, #dynamic flag must be checked on type, not on object itself.

viktormalik
authored and
peterschrammel
committed
Dereference: always add unknown_object when pointer points to multiple dynamic objects.

viktormalik
authored and
peterschrammel
committed
Heap analysis: do RHS 'concretisation' only if heap objects are accessed.

viktormalik
authored and
peterschrammel
committed
solving heap object concretisation in the right-hand side of assignment

martinhruska
authored and
peterschrammel
committed
Do not fail if symbolic dereference cannot be done. Instead, return the original (not dereferenced) expression.

viktormalik
authored and
peterschrammel
committed
Addressing cases where a pointer has (not) been redefined before its dereference appears on the right handed side. Also fixing assignments of right-handed side from a wrong SSA line

martinhruska
authored and
peterschrammel
committed
RHS concretisation: handle when the RHS is an object (and not a member of an object).

viktormalik
authored and
peterschrammel
committed
concretisation also for assertion

martinhruska
authored and
peterschrammel
committed
refactoring concretisation of rhs to a function

martinhruska
authored and
peterschrammel
committed
adding rhs (assertion) concretisation test case

martinhruska
authored and
peterschrammel
committed
recursive concretisation of rhs

martinhruska
authored and
peterschrammel
committed
taking care about assertion in assigments

martinhruska
authored and
peterschrammel
committed
making test case more difficult

martinhruska
authored and
peterschrammel
committed
remember concretisation of rhs

martinhruska
authored and
peterschrammel
committed
k-induction: do not unwind if dynamic objects are present

viktormalik
authored and
peterschrammel
committed
Heap domain: improve updating of rows.

viktormalik
authored and
peterschrammel
committed
Deactivate goto-into-loop unwinding
peterschrammel
committed
Version 0.5.6
peterschrammel
committed

Commits on Nov 20, 2017

Validate witnesses before reporting status
peterschrammel
committed

Commits on Nov 22, 2017

Commits on Nov 25, 2017

Add object-bits dummy option
peterschrammel
committed
Improve calculation of size parameter for malloc.

viktormalik
authored and
peterschrammel
committed
Hack to disable programs containing pointer arithmetics.

viktormalik
authored and
peterschrammel
committed

Commits on Nov 26, 2017

Commits on Nov 27, 2017

Version 0.6.0
peterschrammel
committed

Commits on Jul 17, 2018

Pointed objects: do not create empty object

viktormalik
authored and
peterschrammel
committed
Improve heap domain by tracking symbolic execution paths

viktormalik
authored and
peterschrammel
committed
Add test for the heap domain.

viktormalik
authored and
peterschrammel
committed
Move the function for finding value of a symbolic path into strategy_solver_base

viktormalik
authored and
peterschrammel
committed
Abstract domains: project_on_vars: if vars is empty, return whole abstract value

viktormalik
authored and
peterschrammel
committed
Add concept of symbolic paths

viktormalik
authored and
peterschrammel
committed
Heap-interval domain: improve domain combination

viktormalik
authored and
peterschrammel
committed
Heap domain: undo solving in symbolic paths

viktormalik
authored and
peterschrammel
committed
Add new abstract domain for computing invariants for different symbolic paths

viktormalik
authored and
peterschrammel
committed
Heap domain: if a row is nondet, clear all pointing rows

viktormalik
authored and
peterschrammel
committed
New tests for heap manipulation

viktormalik
authored and
peterschrammel
committed
Fix formatting errors

viktormalik
authored and
peterschrammel
committed
Make map keys non-const

viktormalik
authored and
peterschrammel
committed

Commits on Jul 20, 2018

Commits on Jul 23, 2018

Commits on Jul 26, 2018

Remove debugging output.
viktormalik
committed

Commits on Aug 3, 2018

Commits on Aug 13, 2018

Commits on Aug 14, 2018

Merge pull request #122 from diffblue/release-0.7
peterschrammel
authored

Commits on Sep 29, 2018

Commits on Sep 30, 2018

Commits on Oct 4, 2018

Commits on Nov 13, 2018

Commits on Nov 16, 2018

heap-zones: do not add difference rows for objects allocated by the same malloc
viktormalik
committed

Commits on Nov 19, 2018

Commits on Nov 25, 2018

Update to version 0.7.1
peterschrammel
committed

Commits on Feb 20, 2019

Commits on Mar 20, 2019

Added printing to disjunctive domain class
wadkhlemshem
committed

Commits on Mar 26, 2019

Added project_on_vars
wadkhlemshem
committed

Commits on May 10, 2019

Commits on May 15, 2019

Commits on May 16, 2019

Commits on May 17, 2019

Commits on May 18, 2019

Commits on May 21, 2019

Commits on Aug 28, 2019