| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
it. Don't use pretty warning signs since we can't diff them correctly in the
test output from the test run.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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).
|
| |
|
|
| |
Fortunately, the server spec already assumes an ASCII input channel.
|
| | |
|
| |
|
|
|
| |
This removes the need for special treatment of test input (/trace includes
timings in the output, which are not suitable for tests. /tracePO does not)
|
| | |
|
| |\
| |
| |
| |
| | |
Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.
|
| | |
| |
| |
| |
| |
| | |
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 is useful because trigger-related messages can contain quite a bit of
information, especially if they include info about multiple split quantifiers.
|
| | |
| |
| |
| |
| | |
The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
qunyanm
Clément Pit--Claudel