| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
Thanks Valentin for elucidating this issue!
|
| |
|
|
| |
and #module were not handled
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
time) in the test suite.
Removed some assertions that have been rendered unnecessary because of the computations that Dafny instructs the SMT solver to do.
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
That is, missing expect files now raise a warning, not an error.
|
| |
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
The color fix is only partial. It's rather tricky to support all combinations of
cygwin/cmd and posix/nt Python. At the moment things work well everywhere with
native Python.
|
| | |
| |
| |
| | |
a module import.
|
| |/ |
|
| |
|
|
| |
+ a small fix in runTests.py
|
| |\
| |
| |
| |
| | |
This contains trigger related things under the autoTriggers flag (disabled by
default), and some bug-fixes and cleanups that are already enabled.
|
| | | |
|
| | | |
|
| | | |
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | | |
Found by enabling auto-generated triggers and looking for failing tests
|
| | | | |
|
| | |\| |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
improved the error message reported to users
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
shadow other variables (Issue #86)
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Although
convenient and concise, the auto-declare behavior has on many occasions caused
confusion when a type name has accidentally been mistyped (and Dafny had then
accepted and auto-declared the name).
Note, the behavior of filling in missing type parameters is still supported. This
mode, although unusual (even original?) in languages, is different from the auto-
declare behavior. For auto-declare, identifiers could be used in the program
without having a declaration. For fill-in parameters, the implicitly declared
type parameters remain anonymous.
|
| | | |
|
| | |\ |
|
| | | |
| | |
| | |
| | | |
Improvements in encoding of reads of function values.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
i.e., how many times Z3 is permitted to unfold it's definition. The
new {:fuel} annotation can be added to the function itself, it which
case it will apply to all uses of that function, or it can overridden
within the scope of a module, function, method, iterator, calc, forall,
while, assert, or assume. The general format is:
{:fuel functionName,lowFuel,highFuel}
When applied as an annotation to the function itself, omit functionName.
If highFuel is omitted, it defaults to lowFuel + 1.
The default fuel setting for recursive functions is 1,2. Setting the fuel higher,
say, to 3,4, will give more unfoldings, which may make some proofs go through
with less programmer assistance (e.g., with fewer assert statements), but it may
also increase verification time, so use it with care. Setting the fuel to 0,0 is
similar to making the definition opaque, except when used with all literal arguments.
|
| | | |
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
be a "heap anchor".
Currently, a heap is an anchor if it produced by a havoc (but not a direct update).
|
| | |
| |
| |
| | |
currently unused in the test suite)
|
| |/ |
|
| |
|
|
|
| |
can now assume the precondition (as had also been the case back in the days when
reads clauses had to be self framing).
|
Clément Pit--Claudel
Rustan Leino
Michael Lowell Roberts
Bryan Parno