summaryrefslogtreecommitdiff
path: root/Source/Core/ResolutionContext.cs
Commit message (Collapse)AuthorAge
* Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
|
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-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.
* 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.
* updated the mover checksGravatar qadeer2014-04-25
|
* Add support for assumption variables.Gravatar wuestholz2014-04-21
|
* fixed code contracts violationsGravatar qadeer2014-02-11
|
* added syntax for par call and ParCallCmdGravatar qadeer2013-12-16
|
* extended inlining to deal with codeexprsGravatar qadeer2013-08-14
|
* cleaned up the OG codeGravatar qadeer2013-08-07
| | | | enabled it to be always on
* Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in ↵Gravatar wuestholz2013-07-22
| | | | code (as opposed to contracts).
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
|
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
|
* added parallel callsGravatar Unknown2013-03-01
|
* Removed old comments about "BASEMOVE" and other constructor calls, where the ↵Gravatar Unknown2013-01-07
| | | | conversion from Spec# into C# moved a constructor call
* added support for handling duplicate axiomsGravatar qadeer2011-11-22
|
* convert assert to requiresGravatar qadeer2011-05-16
|
* Boogie: added features to help with modular verification. In particular, ↵Gravatar Rustan Leino2011-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.slnGravatar qadeer2010-12-01
|
* Boogie: Committing changed source filesGravatar tabarbe2010-08-20
|
* Boogie: Renaming core sources in preparation for port commitGravatar tabarbe2010-08-20