summaryrefslogtreecommitdiff
path: root/Source/DafnyDriver
Commit message (Collapse)AuthorAge
* Fix build and test failures, cleanup grammar.Gravatar Richard L. Ford2016-01-27
| | | | | | | | | | 1. A build failure caused by a method call before a contract was fixed. 2. An absolute path in an ".expect" file was changed to relative. 3. I eliminated the TopDecls and DeclModifiers non-terminals. They were giving a warning from Coco/R about being deletable. Instead I used repetition of the TopDecl or DeclModifier non-terminals where they had been used. I think this is also cleaner to talk about.
* Implement 'extern' declaration modifier.Gravatar Richard L. Ford2016-01-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The 'extern' declaration modifier provides a more convenient way of interfacing Dafny code with C# source files and .Net DLLs. We support an 'extern' keyword on a module, class, function method, or method (cannot extern ghost). We check the CompileNames of all modules to make sure there are no duplicate names. Every Dafny-generated C# class is marked partial, so it can potentially be extended. The extern keyword could be accompanied by an optional string naming the corresponding C# method/class to connect to. If not given the name of the method/class is used. An 'extern' keyword implies an {:axiom} attribute for functions and methods, so their ensures clauses are assumed to be true without proof. In addition to the .dfy files, the user may supply C# files (.cs) and dynamic linked libraries (.dll) on command line. These will be passed onto the C# compiler, the .cs files as sources, and the .dll files as references. As part of this change the grammar was refactored some. New productions are - TopDecls - a list of top-level declarations. - TopDecl - a single top-level declaration - DeclModifiers - a list of declaration modifiers which are either 'abstract', 'ghost', 'static', 'protected', or 'extern'. They can be in any order and we diagnose duplicates. In addition, since they are not all allowed in all contexts, we check and give diagnostics if an DeclModifier appears where it is not allowed.
* Fix issue89. Copy the out param to a local before use it in an anonymousGravatar qunyanm2015-11-04
| | | | | | method that is generated by LetExpr. Change the compiler so that each stmt writes to its own buffer before add it to the program's buffer so that we can insert the above mentioned copy instruction before the stmt.
* Fix the build.Gravatar wuestholz2015-09-29
|
* Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience)Gravatar Clément Pit--Claudel2015-08-27
| | | | | | Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it looks for one in Binaries/z3.exe (mostly for backwards-compatibility with already set-up source installations).
* Refactor the error reporting codeGravatar Clément Pit--Claudel2015-08-18
| | | | | The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information.
* Fix: Unify column numbers in Dafny's errorsGravatar Clément Pit--Claudel2015-07-23
| | | | | | | | | Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we print tokens, we need to decrement the column number. This was done for resolver errors, but not for verification or parsing errors. In addition, parsing errors were inconsistent with resolution errors case-wise. Unfortunately, the fix affects the output of many tests.
* Add code to calculate various interesting statistics about Dafny files.Gravatar Bryan Parno2015-07-01
|
* System.Collections.Immutable.dll is now stored in the Binaries directory and ↵Gravatar Michael Lowell Roberts2015-06-16
| | | | copied to the output directory when the /optimize flag is used.
* added -optimize option to compiler.Gravatar Michael Lowell Roberts2015-06-12
|
* Fix the UseBaseNameForFileName flag; it shouldn't set the return code to zero.Gravatar Clément Pit--Claudel2015-06-07
| | | | | The test suite relies on error codes all being zero (except for preprocessing errors), so add a flag for that (as suggested in a source comment).
* MergeGravatar leino2015-01-03
|\
| * Minor changeGravatar wuestholz2014-12-26
| |
* | Fixed bug in /compile:3, when Main is explicitly given as a static methodGravatar leino2014-12-12
|/
* Now the parser parses "Type" rather than "IToken" for a traitGravatar Reza Ahmadi2014-11-05
|
* Create large stack in DafnyDriver.cs, before calling main,Gravatar Bryan Parno2014-10-28
| | | | just in case Boogie needs more room
* Add support for counting spec/impl/proof lines by supressing, e.g., ghost ↵Gravatar Bryan Parno2014-10-27
| | | | statements
* Minor changeGravatar wuestholz2014-10-14
|
* added trait feature:Gravatar Reza Ahmadi2014-07-18
| | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
* Worked on the more advanced verification result caching.Gravatar wuestholz2014-07-10
|
* Added support for verifying Dafny program snapshots from the command-line.Gravatar wuestholz2014-07-01
|
* Minor change due to change in BoogieGravatar wuestholz2014-06-28
|
* Use the new pretty-printing functionality in Boogie. Disable with "/pretty:0"Gravatar Dan Rosén2014-06-24
|
* Fixed issues with absolute file names in the expected output for the lit tests.Gravatar wuestholz2014-06-04
|
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* DafnyExtension: Made it display the compilation output in the VS output pane.Gravatar wuestholz2014-04-21
|
* Supply C# compiler switch /nowarn:0219, which suppresses any warning CS0219 ↵Gravatar Rustan Leino2014-01-13
| | | | about variables not being used.
* Added /compile:3, which compiles in memory and then executes the program (if ↵Gravatar Rustan Leino2014-01-13
| | | | there is a Main and there are no errors). Primarily intended for use with rise4fun.
* Add support for the /verifySeparately flag in Boogie and change most tests ↵Gravatar wuestholz2013-12-18
| | | | to use it.
* Fix build failures due to changes in Boogie.Gravatar wuestholz2013-12-11
|
* Fix some things due to changes in Boogie (execution engine API, ↵Gravatar wuestholz2013-12-09
| | | | 'UnivBackPred2.smt2' no longer needed).
* Fixed build failures due to changes in Boogie.Gravatar wuestholz2013-11-23
|
* Fixed build failure due to changes in Boogie.Gravatar wuestholz2013-10-28
|
* DafnyExtension: Did some refactoring and worked towards integrating the ↵Gravatar wuestholz2013-07-26
| | | | Dafny menu more tightly.
* Did some refactoring of the interaction with the Boogie execution engine.Gravatar wuestholz2013-07-10
|
* Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-24
|
* Fixed a contract.Gravatar wuestholz2013-06-20
|
* Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-19
|
* Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-19
|
* Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-18
|
* DafnyExtension: Cleaned up some references and disabled non-functional ↵Gravatar wuestholz2013-06-07
| | | | support for VS 2010.
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-04
|
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-04
|
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
|
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
|
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
|
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
|
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
|
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
|
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 06:12:55 +0000