summaryrefslogtreecommitdiff
path: root/Test/test0
Commit message (Collapse)AuthorAge
* Boogie:Gravatar rustanleino2010-10-26
| | | | | | | | | * Updated Parser.cs/Scanner.cs to use new .frame files from boogiepartners. * It changes, for example, "syntax error:" to just "error:", so adjusted expected Test outputs. Dafny: * Ditto for its Parser.cs/Scanner.cs. * Added ability to provide a custom Errors handler for scanner/parser. * Added Test/dafny1/Cubes.dfy
* Updated the frame files to work with the latest Coco/R. This entails *not* ↵Gravatar mikebarnett2010-06-22
| | | | | | having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories. Lots of code changes to compensate for the new frame files.
* Allow ":" in addition to "returns" in function definitions. Make the ↵Gravatar MichalMoskal2009-12-17
| | | | | | | | pretty-printer use ":" not "returns". Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions. Consequently foo(int,y:bool) is no longer allowed. Update the testsuite to match that.
* Removed Output files. These are created on a local machine when the tests ↵Gravatar rustanleino2009-08-07
| | | | are run.
* Initial set of files.Gravatar mikebarnett2009-07-15