summaryrefslogtreecommitdiff
path: root/Source/Core/AbsyCmd.cs
Commit message (Collapse)AuthorAge
* Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
|
* Worked on the verification result caching (statement checksums).Gravatar wuestholz2015-01-26
|
* Merging changes from wuestholz/BoogieInvariantFixesIIIIGravatar wuestholz2015-01-13
|\
| * 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 'ListOfMiningStrategies' 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 invariants of classes 'Requires' and 'Ensures' robust by making ↵Gravatar 0biha2014-12-27
|/ | | | 'IPotentialErrorNode' generic.
* Minor changesGravatar wuestholz2015-01-02
|
* Worked on more native support for partially-verified assertions.Gravatar wuestholz2014-12-28
|
* Minor precondition fixGravatar 0biha2014-12-26
|
* 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 'HavocCmd' robust by changing the design (replaced ↵Gravatar 0biha2014-12-19
| | | | public field by private field + getter/setter).
* Made 2 invariants of type 'StateCmd' robust by changing the designGravatar 0biha2014-12-19
| | | | (replaced public fields by private fields + getters/setters).
* Made 2 invariants of type 'AssignCmd' robust byGravatar 0biha2014-12-19
| | | | | | -replacing public fields by private fields + getters/setters, -making setters and constructor create a copy of the arguments, -making getters return read-only lists.
* Reverted a change to CreateTempVariable for FixedPointVC only.Gravatar Ken McMillan2014-12-08
|
* Added todos.Gravatar wuestholz2014-11-26
|
* Worked on the verification result caching (extracted functions).Gravatar wuestholz2014-11-25
|
* Fixed issues in the verification result caching (old expressions).Gravatar wuestholz2014-11-24
|
* Fixed issue in the verification result caching.Gravatar wuestholz2014-11-10
|
* Worked on the verification result caching.Gravatar wuestholz2014-11-10
|
* Made it never include the statement checksum when printing assert statements.Gravatar wuestholz2014-11-16
|
* Minor refactoringGravatar wuestholz2014-11-05
|
* Worked on the verification result caching.Gravatar wuestholz2014-11-05
|
* Made it produce more trace output for the verification result caching.Gravatar wuestholz2014-11-02
|
* Fixed an issue (reported by Akash Lal).Gravatar wuestholz2014-10-30
|
* Worked on the verification result caching.Gravatar wuestholz2014-10-19
|
* Worked on the verification result caching.Gravatar wuestholz2014-10-19
|
* Worked on the verification result caching.Gravatar wuestholz2014-10-17
|
* Worked on the verification result caching.Gravatar wuestholz2014-10-17
|
* Worked on the verification result caching.Gravatar wuestholz2014-10-17
|
* Worked on the verification result caching.Gravatar wuestholz2014-10-17
|
* Minor changeGravatar wuestholz2014-10-16
|
* Worked on the verification result caching.Gravatar wuestholz2014-10-15
|
* Fix issue in computation of checksums for calls.Gravatar wuestholz2014-10-15
|
* Fix issue in computation of checksums for assume statements.Gravatar wuestholz2014-10-14
|
* Implement ToString() override for TransferCmds. It is overriden forGravatar Dan Liew2014-10-13
| | | | | Cmd classes but for some reason it wasn't implemented for TransferCmds which seems a little inconsistent.
* fixed various CodeContracts issues.Gravatar qadeer2014-09-18
|
* Minor refactoringGravatar wuestholz2014-08-03
|
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs.
* Refactored how checksums are computed.Gravatar wuestholz2014-07-13
|
* Worked on the more advanced verification result caching (ignore comments for ↵Gravatar wuestholz2014-07-10
| | | | computing statement checksums).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 05:01:19 +0000