| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | |
|
| | | | |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| | | |
|
| |/ |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| | |
a module import.
|
| |/ |
|
| |\
| |
| |
| |
| | |
This contains trigger related things under the autoTriggers flag (disabled by
default), and some bug-fixes and cleanups that are already enabled.
|
| | | |
|
| | |
| |
| |
| | |
This brings them in line with error column numbers.
|
| | | |
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | | |
Fixed resolution bug where some type arguments were not checked to have been determined.
Fixed resolution bugs where checking for equality-supporting types was missing.
|
| | | |
| | |
| | |
| | |
| | | |
This is a temporary measure to ensure that the trigger related machinery
is entirely disabled when /autoTriggers is off.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The problem was that inlining would replace formals with arguments in triggers
as well, causing invalid expressions ("trigger killers") to pop up in triggers
after inlining.
This fix disables inlining if it can't be determined that it won't lead to an
invalid trigger. If that procedure is incomplete, then that's only by a narrow
margin, as the checks actually ensure that the formals that are getting trigger
killers are indeed used in triggers.
|
| | | |
| | |
| | |
| | |
| | | |
Stop using HashSet, as we don't currently have a good HashCode implementation.
Instead, excplicitly call distinct where needed. Improve reporting a bit.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
Includes trigger generation, basic cycle detection, and basic equality
comparison for Dafny expressions.
|
| | | |
| | |
| | |
| | | |
Use an extension method to properly deal with null attributes
|
| | |/ |
|
| | |
| |
| |
| | |
improved the error message reported to users
|
| | | |
|
| | | |
|
leino
Clément Pit--Claudel
Michael Lowell Roberts