| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
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).
|
|
|
|
|
| |
The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
copied to the output directory when the /optimize flag is used.
|
| |
|
|
|
|
|
| |
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).
|
|\ |
|
| | |
|
|/ |
|
| |
|
|
|
|
| |
just in case Boogie needs more room
|
|
|
|
| |
statements
|
| |
|
|
|
|
|
|
| |
-possibility to declare traits in Dafny
-possibility to extend a class by a trait
-possibility to override body-less methods
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
about variables not being used.
|
|
|
|
| |
there is a Main and there are no errors). Primarily intended for use with rise4fun.
|
|
|
|
| |
to use it.
|
| |
|
|
|
|
| |
'UnivBackPred2.smt2' no longer needed).
|
| |
|
| |
|
|
|
|
| |
Dafny menu more tightly.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
support for VS 2010.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|