Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fixed a postcondition. | 2014-12-26 | |
| | |||
* | Added an annotation, :split_here, for predicate statements. | 2014-12-16 | |
| | | | | | | The annotation allows the programmer to manually indicate where the verification of a procedure implementation should be split into pieces. | ||
* | Merge some FixpointVC changes that got left behind | 2014-12-08 | |
|\ | |||
* | | Optimized the VC generation for assumption variables. | 2014-12-07 | |
| | | |||
* | | Fixed issue in the verification result caching. | 2014-11-10 | |
| | | |||
* | | Worked on the verification result caching. | 2014-11-10 | |
| | | |||
* | | Worked on the verification result caching. | 2014-11-05 | |
| | | |||
* | | Worked on the verification result caching. | 2014-11-03 | |
| | | |||
* | | Worked on the verification result caching. | 2014-11-03 | |
| | | |||
* | | Fixed minor issue. | 2014-11-02 | |
| | | |||
* | | Made it produce more trace output for the verification result caching. | 2014-11-02 | |
| | | |||
* | | Did some refactoring. | 2014-11-02 | |
| | | |||
* | | SI: print if a bound was reached. | 2014-10-29 | |
| | | |||
* | | Worked on the verification result caching. | 2014-10-19 | |
| | | |||
* | | Worked on the verification result caching. | 2014-10-19 | |
| | | |||
* | | Did some refactoring. | 2014-10-18 | |
| | | |||
* | | Made it produce more trace output for the verification result caching. | 2014-10-18 | |
| | | |||
* | | Worked on the verification result caching. | 2014-10-17 | |
| | | |||
* | | Worked on the verification result caching. | 2014-10-17 | |
| | | |||
* | | Did some refactoring. | 2014-10-16 | |
| | | |||
* | | Worked on the verification result caching. | 2014-10-16 | |
| | | |||
* | | Fix issue in verification result caching. | 2014-10-15 | |
| | | |||
* | | Fix issue in verification result caching. | 2014-10-15 | |
| | | |||
* | | Made it produce more trace output for the verification result caching. | 2014-10-14 | |
| | | |||
* | | Fix issue in verification result caching for assertions without subsumption. | 2014-10-13 | |
| | | |||
* | | Add a todo. | 2014-10-13 | |
| | | |||
| * | Merge FixpointVC changes with mainline | 2014-10-08 | |
|/| | |||
| * | Added "extra recursion bound" to FixedpointVC to support Corral. | 2014-10-08 | |
| | | |||
* | | Merge | 2014-10-01 | |
|\ \ | |||
| * | | Minor corrections | 2014-10-01 | |
| | | | |||
* | | | fixed StackOverflow in TraceCounterexample; | 2014-09-30 | |
|/ / | | | | | | | converted tail recursion into a loop | ||
* | | SI: VC gen with labels | 2014-09-29 | |
| | | |||
* | | Cleanup: removed unused code | 2014-09-29 | |
| | | |||
* | | Fix to VC gen | 2014-09-28 | |
| | | |||
* | | Fix for boolVC generation | 2014-09-27 | |
| | | |||
* | | Lets have a setter for TopLevelDeclarations as well | 2014-09-25 | |
| | | |||
* | | (Subhajit) Added an interface for InterpolatingTheoremProver | 2014-09-24 | |
| | | |||
* | | minor fix | 2014-09-24 | |
| | | |||
* | | Simple VC generation for SI | 2014-09-24 | |
| | | |||
* | | Fixed assertion violation. | 2014-09-23 | |
| | | |||
* | | Did more refactoring and addressed several todos. | 2014-09-23 | |
| | | |||
* | | Did more refactoring. | 2014-09-23 | |
| | | |||
* | | Did some refactoring. | 2014-09-23 | |
| | | |||
* | | Fixed an issue in the verification result caching (recycled errors). | 2014-09-22 | |
| | | |||
* | | fixed various CodeContracts issues. | 2014-09-18 | |
|/ | |||
* | merge | 2014-08-08 | |
|\ | |||
* | | fixed codexpr bug reported by Michael Emmi; removed special handling of ↵ | 2014-08-08 | |
| | | | | | | | | codexpr in InjectPostConditions | ||
| * | Bug fix in SI | 2014-08-03 | |
|/ | |||
* | Some simplifications | 2014-07-28 | |
| | |||
* | Fix nasty bug introduced by commit 61a94f409975. | 2014-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. |