| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
until the editor is idle for 5 second.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
half a second, but delay calling Dafny resolver until the text buffer hasn't
been changed for 5 seconds. Also save the parsing result from TokenTagger in
ITextBuffer's property instead of in a static field.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- cache scan results so it can be shared between different instances of
DafnyTokenTagger
- Instead of rescanning the whole text buffer upon a text change, only rescan
the text span that the text change is in.
- set the timer to half a second to match the comment at the beginnig of
the file. The event change are only passed along to Dafny when the user stop
typing for half a second.
- Change framework dependence so the project can work with version 4.5 and
higher.
|
| |
|
|
| |
identifiers
|
| |
|
|
| |
Rustan).
|
| | |
|
| |
|
|
|
|
| |
verification
errors (previously, verification errors were masked by resolution warnings)
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
(This also undoes two previous attempted fixes, which had accidentally disabled some outlining and hovertexts.)
|
| | |
|
| |
|
|
|
|
|
|
| |
The VS extension already did that, but it also filtered out nested tokens. That
prevented info about triggers from being reported. Other interfaces (the CLI
and Emacs, in particular) should have the same ability.
Surprinsingly, this doesn't cause any tests failures.
|
| | |
|
| |
|
|
|
| |
The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.
|
| | |
|
| |
|
|
|
|
| |
The error came from the fact that Dafny now consistently used 0-based indexing.
Boogie gets its traces from text that's inserted by Dafny in the Boogie file, so
there's no need to apply an extra offset in the VS extension.
|
| | |
|
| | |
|
| |
|
|
|
| |
To check if the fix works, try declaring a static top level function.
Initial work on this patch by Rustan
|
| |
|
|
|
| |
BoundVars that are combined in rewriting of the nested match patterns so they
show up in the IDE correctly.
|
| |
|
|
| |
explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Source/DafnyExtension directory) as pre-build events
|
| | |
|
| |
|
|
| |
my previous checkin)
|
| |
|
|
| |
command-line options from DafnyOptions.txt during initialization. DafnyOptions.txt gets built into the VSIX file and is installed as part of the Dafny Visual Studio extension.
|
| | |
|
| | |
|
| |
|
|
| |
default.
|
| | |
|
| | |
|
| |
|
|
| |
included by another command-line file.
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings.
Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions.
Fixed lack of operator resolution in custom attributes.
|
| |/ |
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/ |
|
| |
|
|
|
| |
Added IsGoodHeap antecedent in (exists heap ...) in newtype Is axioms.
Added IDE tool tips in newtype constraints.
|
| |
|
|
| |
Added parsing of constraints (beyond parsing is yet to come)
|
| | |
|
qunyanm
Richard L. Ford
Bryan Parno
Clément Pit--Claudel