Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge remote-tracking branch 'refs/remotes/origin/dafny-bug-fix' | qunyanm | 2015-11-25 |
|\ | |||
* \ | Merge remote-tracking branch 'refs/remotes/origin/dafny-bug-fix' | qunyanm | 2015-11-25 |
|\ \ | |||
| | * | Use the EndCurly token when creating the ReturnCmd for unifiedExit | qunyanm | 2015-11-25 |
| |/ | | | | | | | | | | | | | | | When there are more than one exit blocks, an unified exit block is created which includes a ReturnCmd. However, the ReturnCmd is created with NoToken. This causes the line/column number reported for a failed postcondition to be (0,0). The right token should be the EndCurly since the ReturnCmd is in the exit block. | ||
* | | Fix issue with partially-verified assertions. | Valentin Wüstholz | 2015-11-19 |
| | | |||
* | | Add experimental support for optimization (requires Z3 build after changeset ↵ | Valentin Wüstholz | 2015-11-18 |
| | | | | | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
| * | Use EndCurly token for the ReturnCmd when creating unifiedExit | qunyanm | 2015-11-16 |
| | | | | | | | | | | Instead of using NoToken for the ReturnCmd, use the EndCurly, if it exists, when creating unifiedExit | ||
| * | Use EndCurly token for the ReturnCmd when creating unifiedExit | qunyanm | 2015-11-16 |
|/ | | | | | Instead of using NoToken for the ReturnCmd, use the EndCurly when creating unifiedExit. | ||
* | Improve output for diagnosing timeouts. | Valentin Wüstholz | 2015-09-30 |
| | |||
* | Normalise line endings using a .gitattributes file. Unfortunately | Dan Liew | 2015-06-28 |
| | | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. | ||
* | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-06-05 |
| | |||
* | Make caching of verification results more fine-grained for changes that ↵ | Valentin Wüstholz | 2015-05-17 |
| | | | | affect preconditions. | ||
* | Make it preserve the fact that the value of an assumption variable never ↵ | Valentin Wüstholz | 2015-05-06 |
| | | | | becomes logically weaker after a havoc. | ||
* | Made it produce slightly different passive commands for assignments to ↵ | wuestholz | 2015-01-30 |
| | | | | assumption variables. | ||
* | Worked on the verification result caching (trace output). | wuestholz | 2015-01-26 |
| | |||
* | Worked on the verification result caching (use native support for partially ↵ | wuestholz | 2015-01-16 |
| | | | | verified assertions). | ||
* | Fix related to limitations in CVC4 model parsing | Ally Donaldson | 2015-01-14 |
| | |||
* | Worked on more native support for partially-verified assertions. | wuestholz | 2014-12-28 |
| | |||
* | Optimized the VC generation for assumption variables. | wuestholz | 2014-12-07 |
| | |||
* | Fixed issue in the verification result caching. | wuestholz | 2014-11-10 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-11-10 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-11-05 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-11-03 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-11-03 |
| | |||
* | Fixed minor issue. | wuestholz | 2014-11-02 |
| | |||
* | Made it produce more trace output for the verification result caching. | wuestholz | 2014-11-02 |
| | |||
* | Did some refactoring. | wuestholz | 2014-11-02 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-10-19 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-10-19 |
| | |||
* | Did some refactoring. | wuestholz | 2014-10-18 |
| | |||
* | Made it produce more trace output for the verification result caching. | wuestholz | 2014-10-18 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-10-17 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-10-17 |
| | |||
* | Did some refactoring. | wuestholz | 2014-10-16 |
| | |||
* | Worked on the verification result caching. | wuestholz | 2014-10-16 |
| | |||
* | Fix issue in verification result caching. | wuestholz | 2014-10-15 |
| | |||
* | Fix issue in verification result caching. | wuestholz | 2014-10-15 |
| | |||
* | Made it produce more trace output for the verification result caching. | wuestholz | 2014-10-14 |
| | |||
* | Fix issue in verification result caching for assertions without subsumption. | wuestholz | 2014-10-13 |
| | |||
* | Add a todo. | wuestholz | 2014-10-13 |
| | |||
* | Fixed assertion violation. | wuestholz | 2014-09-23 |
| | |||
* | Did some refactoring. | wuestholz | 2014-09-23 |
| | |||
* | Fixed an issue in the verification result caching (recycled errors). | wuestholz | 2014-09-22 |
| | |||
* | fixed various CodeContracts issues. | qadeer | 2014-09-18 |
| | |||
* | fixed codexpr bug reported by Michael Emmi; removed special handling of ↵ | qadeer | 2014-08-08 |
| | | | | codexpr in InjectPostConditions | ||
* | Fix nasty bug introduced by commit 61a94f409975. | Dan Liew | 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. | ||
* | Worked on the more advanced verification result caching. | wuestholz | 2014-07-10 |
| | |||
* | Worked on the more advanced verification result caching. | wuestholz | 2014-07-10 |
| | |||
* | Worked on the more advanced verification result caching. | wuestholz | 2014-07-09 |
| | |||
* | Worked on adding support for "canned errors". | wuestholz | 2014-07-07 |
| | |||
* | Added more tests and worked on adding support for "canned errors". | wuestholz | 2014-07-06 |
| |