| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
z3 doesn't support byte-order marks; thus using the default UTF8Encoding object
(to allow printing nice warning signs) causes issues, as it sends a BOM before
anything else.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
This allows it to report the source of the error, giving better feedback to the
user about which precondition to a function failed to hold, for example.
|
| | |
|
| |
|
|
|
| |
In particular, start detecting loops between terms that don't look like each
other at the Dafny level, such as {a[x]} and {x in a} (when a is a multiset)
|
| |
|
|
|
| |
This is useful because trigger-related messages can contain quite a bit of
information, especially if they include info about multiple split quantifiers.
|
| | |
|
| |
|
|
|
|
|
|
|
| |
This requires rewriting the parts of the AST that contain these quantifiers. We
unfortunately don't have facilities to do such rewrites at the moment (and there
are loops in the AST, so it would be hard to write such a facility). As a
workaround, this commit introduces a field in quantifier expressions,
SplitQuantifiers. Code that manipulate triggers is expected to look for this
field, and ignore the other fields if that one is found.
|
| |
|
|
|
|
|
|
|
|
| |
Implementing loop detection between multiple triggers is much harder, as it
seems to require walking an exponentially sized graph. Self-loop detection is
still a net gain compared to the current situation: we used to not detect loops
in large quantifiers; not we break these apart, suppress the loops where we can
in the smaller parts, and report the ones that we can't suppress. It could be
that the broken-up quantifiers are mutually recursive, but these cases would
have already led to a loop in the past.
|
| | |
|
| | |
|
| |
|
|
| |
This new version will include a cleaner pipeline, and trigger splitting.
|
| |
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| | | |
|
| | |\ |
|
| | | |\
| |_|/
|/| | |
|
| | | |\ |
|
| | | |/
| |/| |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| | |
The confusing part here is that if one passes null as the ProgramId for two
consecutive calls to Boogie, then Boogie will return the same results twice,
regardless of what the second program was.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The Dafny server is a command line utility that allows non-.Net editors to take
advantage of Dafny's caching facilities, as used by the Dafny extension for
Visual Studio. The server is essentially a REPL, which produces output in the
same format as the Dafny CLI; clients thus do not need to understand the
internals of Dafny's caching. A typical editing session proceeds as follows:
* When a new Dafny file is opened, the editor starts a new instance of the
Dafny server. The cache is blank at that point.
* The editor sends a copy of the buffer for initial verification. This takes
some time, after which the server returns a list of errors.
* The user makes modifications; the editor periodically sends a new copy of
the buffer's contents to the Dafny server, which quickly returns an updated
list of errors.
The client-server protocol is sequential, uses JSON, and works over ASCII
pipes by base64-encoding queries. It defines one type of query, and two types
of responses:
Queries are of the following form:
verify
<base64 encoded JSON payload>
[[DAFNY-CLIENT: EOM]]
Responses are of the following form:
<list of errors and usual output, as produced by the Dafny CLI>
[SUCCESS] [[DAFNY-SERVER: EOM]]
or
<error message>
[FAILURE] [[DAFNY-SERVER: EOM]]
The JSON payload is an array with 4 fields:
* args: An array of Dafny arguments, as passed to the Dafny CLI
* source: A Dafny program, or the path to a Dafny source file.
* sourceIsFile: A boolean indicating whether the 'source' argument is a
Dafny program or the path to one.
* filename: The name of the original source file, to be used in error
messages
For small files, embedding the Dafny source directly into a message is
convenient; for larger files, however, it is generally better for performance
to write the source snapshot to a separate file, and to pass that to Dafny
by setting the 'sourceIsFile' flag to true.
|
| | |
| |
| |
| | |
and #module were not handled
|
| | | |
|
| |\ \ |
|
| | |/
| |
| |
| | |
that Coco.exe is now included in boogiepartners.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
There now is one main entry point for reporting errors, warnings, or
information. Next step is to make the VS extension use that.
|
| |/
|
|
| |
Signed-off-by: Clement Pit--Claudel <clement.pitclaudel@live.com>
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
The function IgnoreFuel in UnfoldingPerformance.dfy used to be lit-wrapped. It
shouldn't be, because its reads clause is non-empty. This is not a soundness
bug, but fixing it improves performance in cases where a function call would be
incorrectly unrolled.
Test case written by Rustan.
|
| | |
| |
| |
| |
| |
| |
| | |
If /useBasenameForFilename is specified, tokens just contain file names, which
is not enough to locate included files.
Solution based on Rustan's advice.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
To check if the fix works, try declaring a static top level function.
Initial work on this patch by Rustan
|
| | |
| |
| |
| |
| | |
- diabled error message related to ensures clauses requiring function bodies in the case of abstract modules.
- fixed bug in similar error message related to bodyless methods in abstract modules.
|
| |\| |
|
| | | |
|
| | | |
|
Clément Pit--Claudel
Rustan Leino
Michael Lowell Roberts