| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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).
|
| |
|
|
|
|
| |
Test/dafny0/Reads.dfy for benefits.
(Unfortunately, this loses track of the "postcondition might not hold on this return path" locations, see Test/dafny0/FunctionSpecifications.dfy.)
|
| | |
|
| | |
|
| |
|
|
| |
precondition has otherwise been checked for well-formedness
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The problem was this:
Console.WriteLine(Int64.Parse("08000000000000000", NumberStyles.HexNumber));
// => -9223372036854775808
Console.WriteLine(Int64.Parse("9223372036854775808"));
// => Value was either too large or too small for an Int64.
In other words, large hex numbers are interpreted as a sequence of bits, not as
an actual number.
|
| |\| |
|
| | |
| |
| |
| | |
allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change)
|
| | |\ |
|
| | | | |
|
Rustan Leino
Clément Pit--Claudel
Michael Lowell Roberts
Bryan Parno