| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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
|
| | | |
|
| | | |
|
| | |\ |
|
| | | |
| | |
| | |
| | | |
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.
|
| | |/
| |
| |
| |
| | |
- fix for requirement inheritance in refinement.
- minimimally viable implementation of exclusive refinement feature.
|
| | |\ |
|
| | | | |
|
| | | | |
|
| | |\| |
|
| | | |
| | |
| | |
| | | |
Improvements in encoding of reads of function values.
|
| | | |
| | |
| | |
| | | |
at least for some common expressions.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |\ |
|
| | |/ /
|/| | |
|
| | |/ |
|
| |/
|
|
|
| |
BoundVars that are combined in rewriting of the nested match patterns so they
show up in the IDE correctly.
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
be a "heap anchor".
Currently, a heap is an anchor if it produced by a havoc (but not a direct update).
|
| | |
| |
| |
| | |
when the datetype is not null.
|
| |/ |
|
| |\ |
|
| | |
| |
| |
| | |
copied to the output directory when the /optimize flag is used.
|
| | |
| |
| |
| |
| | |
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)
|
| |/ |
|
| |
|
|
|
|
|
| |
Mono currently does not implement support for BigInteger.Parse, so use Int64 if
possible, and throw the same error as was previously returned otherwise. This is
not too much of a problem in practice, because most of the integers that we
actually come across in real-life source files seem to fit in an Int64.
|
| |\ |
|
| | |
| |
| |
| |
| | |
rather than xor. The latter produces pessimal performance if the
datatype contains duplicate data.
|
| | | |
|
| |/
|
|
|
| |
The test suite relies on error codes all being zero (except for preprocessing
errors), so add a flag for that (as suggested in a source comment).
|
| | |
|
| |
|
|
| |
explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations.
|
| |\ |
|
| | | |
|
Clément Pit--Claudel
Michael Lowell Roberts
Rustan Leino
Bryan Parno