Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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. | ||
* | updated the mover checks | qadeer | 2014-04-25 |
| | |||
* | Add support for assumption variables. | wuestholz | 2014-04-21 |
| | |||
* | fixed code contracts violations | qadeer | 2014-02-11 |
| | |||
* | added syntax for par call and ParCallCmd | qadeer | 2013-12-16 |
| | |||
* | extended inlining to deal with codeexprs | qadeer | 2013-08-14 |
| | |||
* | cleaned up the OG code | qadeer | 2013-08-07 |
| | | | | enabled it to be always on | ||
* | Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in ↵ | wuestholz | 2013-07-22 |
| | | | | code (as opposed to contracts). | ||
* | Started to remove ...Seq classes | Ally Donaldson | 2013-07-22 |
| | |||
* | More refactoring towards replacing PureCollections.Sequence with List | Ally Donaldson | 2013-07-22 |
| | |||
* | added parallel calls | Unknown | 2013-03-01 |
| | |||
* | Removed old comments about "BASEMOVE" and other constructor calls, where the ↵ | Unknown | 2013-01-07 |
| | | | | conversion from Spec# into C# moved a constructor call | ||
* | added support for handling duplicate axioms | qadeer | 2011-11-22 |
| | |||
* | convert assert to requires | qadeer | 2011-05-16 |
| | |||
* | Boogie: added features to help with modular verification. In particular, ↵ | Rustan Leino | 2011-05-13 |
| | | | | define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations. | ||
* | Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln | qadeer | 2010-12-01 |
| | |||
* | Boogie: Committing changed source files | tabarbe | 2010-08-20 |
| | |||
* | Boogie: Renaming core sources in preparation for port commit | tabarbe | 2010-08-20 |