summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* MergeGravatar Ally Donaldson2015-01-13
|\
| * Merging changes from wuestholz/BoogieInvariantFixesIIIIGravatar wuestholz2015-01-13
| |\
| * \ Merging changes from 0biha/BoogieInvariantFixesIIIaGravatar wuestholz2015-01-13
| |\ \
* | | | Removed unnecessary stage-related attributes from candidate annotations.Gravatar Ally Donaldson2015-01-10
| | | |
| | | * Made 2 invariants of class 'VariableCollector' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field protected - exposing IEnumerables (with help from David Rohr)
| | | * Made invariant of class 'Trigger' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - adding getter/setter - copying incoming list - exposing read-only list (with help from David Rohr)
| | | * Made invariant of class 'StmtList' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private and readonly - exposing IEnumerable - adding 'AddLabel' method (with help from David Rohr)
| | | * Made invariant of class 'StmtList' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - adding private field - exposing read-only list - copying incoming list (with help from David Rohr)
| | | * Made invariant of class 'QKeyValue' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing read-only list - copying incoming list - adding methods 'AddParam', 'AddParams', and 'ClearParams' (with help from David Rohr)
| | | * Made invariant of class 'EEDTemplate' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable - copying incoming list (with help from David Rohr)
| | | * Made invariant of class 'Block' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable (with help from David Rohr)
| | | * Made invariant of class CommandLineOptions robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable (with help from David Rohr)
| | | * Made 2 invariants of class 'CommandLineOptions' robust by:Gravatar wuestholz2015-01-09
| | |/ | |/| | | | | | | | | | | | | | | | - making fields private - exposing IEnumerables - adding methods 'AddProverOption', 'RemoveAllProverOptions', and 'AddZ3Option' (with help from David Rohr)
| * | Minor changes to the "Checked" build configurationGravatar wuestholz2015-01-09
|/ /
| * Tiny change ('Trigger' class)Gravatar 0biha2015-01-08
| |
* | Updated to Staged HoudiniGravatar Ally Donaldson2015-01-08
| |
| * Fixed a null reference problem in class 'Constant'.Gravatar 0biha2015-01-08
| |
| * Tiny fix (made field 'tr' of class 'Trigger' private)Gravatar 0biha2015-01-08
| |
| * Made 2 invariants of class 'DeclWithFormals' robust by changing the designGravatar 0biha2015-01-07
| | | | | | | | (replaced public fields by private fields + getters/setters)
| * Rewrote 'globalVariablesCache' invariant fix of class 'Program'Gravatar 0biha2015-01-08
| |
| * Made invariant of class 'Constant' robust by making list 'Parents' read-onlyGravatar 0biha2015-01-05
| |
| * Made invariant of class 'AtomicRE' robust by changing the designGravatar 0biha2015-01-05
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made invariant of class 'Trigger' robust byGravatar 0biha2015-01-01
| | | | | | | | | | | | -replacing public field by private field + getter -using read-only wrappers (to avoid leaking) -cloning the tr list in the setter and constructor (to avoid capturing)
| * Made invariant of class 'ListOfMiningStrategies' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made invariant of class 'IfThenElse' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made 2 invariants of class 'IfCmd' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public fields by private fields + getters/setters)
| * Made invariant of class 'EEDTemplate' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made invariant of class 'StructuredCmd' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made 2 invariants of class 'Block' robust by changing the designGravatar 0biha2015-01-08
| | | | | | | | (replaced public fields by private fields + getters/setters)
| * Made 3 invariants of class 'BigBlock' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public fields by private fields + getters/setters)
| * Made invariant of class 'CommandLineOptions' robust by changing the designGravatar 0biha2014-12-31
| | | | | | | | (replaced public variable by private variable + getter/setter).
| * Made invariant of class 'CommandLineOptions' robust by changing the designGravatar 0biha2015-01-08
| | | | | | | | (replaced public variable by private variable + getter/setter).
| * Made invariant of class 'Program' robust by making the GlobalVariables cache ↵Gravatar 0biha2014-12-27
| | | | | | | | read-only.
| * Made invariants of classes 'Requires' and 'Ensures' robust by making ↵Gravatar 0biha2014-12-27
|/ | | | 'IPotentialErrorNode' generic.
* Minor changesGravatar wuestholz2015-01-02
|
* Added a test and a todo.Gravatar wuestholz2015-01-02
|
* Worked on more native support for partially-verified assertions.Gravatar wuestholz2014-12-28
|
* Minor change in verification result caching (extracted functions)Gravatar wuestholz2014-12-28
|
* Merging changes from 0biha/BoogieInvariantFixesIIGravatar wuestholz2014-12-27
|\
* \ MergeGravatar 0biha2014-12-26
|\ \
| | * MergeGravatar 0biha2014-12-26
| | |\ | | |/ | |/|
| | * Minor precondition fixGravatar 0biha2014-12-26
| | |
| * | Minor changeGravatar wuestholz2014-12-26
| | |
| * | Fixed a postcondition.Gravatar wuestholz2014-12-26
| | |
| * | strengthened type checkingGravatar qadeer2014-12-26
| | | | | | | | | | | | | | | cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions
| | * Replaced properties Lhss_NRO and Rhss_NRO by methods SetLhs and SetRhs.Gravatar 0biha2014-12-25
| | |
| | * Made some compatibility fixes after running the unit tests.Gravatar 0biha2014-12-24
| | | | | | | | | | | | Added an internal non-readonly version of Lhss and Rhss to 'AssignCmd'.
| | * Made invariant of class 'CommandLineOptions' robust by changing the designGravatar 0biha2014-12-24
| | | | | | | | | | | | (made field 'Ai' read-only).
| | * Backed out changeset: 4103d2e9c2efGravatar 0biha2014-12-24
| | |
| | * Scanner generation with CocoGravatar 0biha2014-12-24
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-29 16:59:49 +0000