Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Fix related to limitations in CVC4 model parsing | 2015-01-14 | ||
| | | ||||
| * | Merge | 2015-01-13 | ||
| |\ | ||||
| | * | Merging changes from wuestholz/BoogieInvariantFixesIIII | 2015-01-13 | ||
| | |\ | ||||
| | * | | Merging changes from 0biha/BoogieInvariantFixesIIIa | 2015-01-13 | ||
| |/| | |/| | | | ||||
| * | | | Removed unnecessary stage-related attributes from candidate annotations. | 2015-01-10 | ||
| | | | | ||||
| | | * | Made 2 invariants of class 'VariableCollector' robust by: | 2015-01-09 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | - making field protected - exposing IEnumerables (with help from David Rohr) | |||
| | | * | Made invariant of class 'Trigger' robust by: | 2015-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: | 2015-01-09 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private and readonly - exposing IEnumerable - adding 'AddLabel' method (with help from David Rohr) | |||
| | | * | Made invariant of class 'StmtList' robust by: | 2015-01-09 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | - adding private field - exposing read-only list - copying incoming list (with help from David Rohr) | |||
| | | * | Made invariant of class 'QKeyValue' robust by: | 2015-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: | 2015-01-09 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable - copying incoming list (with help from David Rohr) | |||
| | | * | Made invariant of class 'Block' robust by: | 2015-01-09 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable (with help from David Rohr) | |||
| | | * | Made invariant of class CommandLineOptions robust by: | 2015-01-09 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable (with help from David Rohr) | |||
| | | * | Made 2 invariants of class 'CommandLineOptions' robust by: | 2015-01-09 | ||
| |_|/ |/| | | | | | | | | | | | | | | | | | - making fields private - exposing IEnumerables - adding methods 'AddProverOption', 'RemoveAllProverOptions', and 'AddZ3Option' (with help from David Rohr) | |||
* | | | Minor changes to the "Checked" build configuration | 2015-01-09 | ||
|/ / | ||||
| * | Tiny change ('Trigger' class) | 2015-01-08 | ||
| | | ||||
* | | Updated to Staged Houdini | 2015-01-08 | ||
| | | ||||
| * | Fixed a null reference problem in class 'Constant'. | 2015-01-08 | ||
| | | ||||
| * | Tiny fix (made field 'tr' of class 'Trigger' private) | 2015-01-08 | ||
| | | ||||
| * | Made 2 invariants of class 'DeclWithFormals' robust by changing the design | 2015-01-07 | ||
| | | | | | | | | (replaced public fields by private fields + getters/setters) | |||
| * | Rewrote 'globalVariablesCache' invariant fix of class 'Program' | 2015-01-08 | ||
| | | ||||
| * | Made invariant of class 'Constant' robust by making list 'Parents' read-only | 2015-01-05 | ||
| | | ||||
| * | Made invariant of class 'AtomicRE' robust by changing the design | 2015-01-05 | ||
| | | | | | | | | (replaced public field by private field + getter/setter) | |||
| * | Made invariant of class 'Trigger' robust by | 2015-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 design | 2015-01-01 | ||
| | | | | | | | | (replaced public field by private field + getter/setter) | |||
| * | Made invariant of class 'IfThenElse' robust by changing the design | 2015-01-01 | ||
| | | | | | | | | (replaced public field by private field + getter/setter) | |||
| * | Made 2 invariants of class 'IfCmd' robust by changing the design | 2015-01-01 | ||
| | | | | | | | | (replaced public fields by private fields + getters/setters) | |||
| * | Made invariant of class 'EEDTemplate' robust by changing the design | 2015-01-01 | ||
| | | | | | | | | (replaced public field by private field + getter/setter) | |||
| * | Made invariant of class 'StructuredCmd' robust by changing the design | 2015-01-01 | ||
| | | | | | | | | (replaced public field by private field + getter/setter) | |||
| * | Made 2 invariants of class 'Block' robust by changing the design | 2015-01-08 | ||
| | | | | | | | | (replaced public fields by private fields + getters/setters) | |||
| * | Made 3 invariants of class 'BigBlock' robust by changing the design | 2015-01-01 | ||
| | | | | | | | | (replaced public fields by private fields + getters/setters) | |||
| * | Made invariant of class 'CommandLineOptions' robust by changing the design | 2014-12-31 | ||
| | | | | | | | | (replaced public variable by private variable + getter/setter). | |||
| * | Made invariant of class 'CommandLineOptions' robust by changing the design | 2015-01-08 | ||
| | | | | | | | | (replaced public variable by private variable + getter/setter). | |||
| * | Made invariant of class 'Program' robust by making the GlobalVariables cache ↵ | 2014-12-27 | ||
| | | | | | | | | read-only. | |||
| * | Made invariants of classes 'Requires' and 'Ensures' robust by making ↵ | 2014-12-27 | ||
|/ | | | | 'IPotentialErrorNode' generic. | |||
* | Minor changes | 2015-01-02 | ||
| | ||||
* | Added a test and a todo. | 2015-01-02 | ||
| | ||||
* | Worked on more native support for partially-verified assertions. | 2014-12-28 | ||
| | ||||
* | Minor change in verification result caching (extracted functions) | 2014-12-28 | ||
| | ||||
* | Merging changes from 0biha/BoogieInvariantFixesII | 2014-12-27 | ||
|\ | ||||
* \ | Merge | 2014-12-26 | ||
|\ \ | ||||
| | * | Merge | 2014-12-26 | ||
| | |\ | | |/ | |/| | ||||
| | * | Minor precondition fix | 2014-12-26 | ||
| | | | ||||
| * | | Minor change | 2014-12-26 | ||
| | | | ||||
| * | | Fixed a postcondition. | 2014-12-26 | ||
| | | | ||||
| * | | strengthened type checking | 2014-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. | 2014-12-25 | ||
| | | | ||||
| | * | Made some compatibility fixes after running the unit tests. | 2014-12-24 | ||
| | | | | | | | | | | | | Added an internal non-readonly version of Lhss and Rhss to 'AssignCmd'. | |||
| | * | Made invariant of class 'CommandLineOptions' robust by changing the design | 2014-12-24 | ||
| | | | | | | | | | | | | (made field 'Ai' read-only). | |||
| | * | Backed out changeset: 4103d2e9c2ef | 2014-12-24 | ||
| | | |