| Commit message (Collapse) | Author | Age |
|\ |
|
| |
| |
| |
| |
| |
| | |
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.
|
|\ |
|
| | |
|
|\| |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
function last<T>(xs: List<T>): T
requires xs != Nil
{
match xs
case Cons(y, Nil) => y
case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
}
And
function minus(x: Nat, y: Nat): Nat
{
match (x, y)
case (Zero, _) => Zero
case (Suc(_), Zero) => x
case (Suc(a), Suc(b)) => minus(a, b)
}
|
| |/
|/|
| |
| |
| |
| | |
Debug version of the projects (rather than Checked).
The Checked build still builds the Checked version of the projects.
|
| | |
|
| |
| |
| |
| |
| |
| | |
Fix bug with not seeing imap's because of type synonyms.
Don't show semi-colon after "decreases" in hover text.
Minor cosmetic change in a test case.
|
| | |
|
| | |
|
| |
| |
| |
| | |
corresponding incorrectly recorded desired answer)
|
| |
| |
| |
| | |
provable.
|
| | |
|
|\| |
|
| |
| |
| |
| | |
function has a MemberSelectExpr that accesses a type with only one constructor.
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
of ambiguous names that arise
when layers of modules are opened-imported don't cause gross memory waste. In particular, previously, the
names of many such ambiguous declarations were shown to exceed 1 million characters, the way they had been
constructed. Now, multiple imports of the same declaration are immediatley resolved as not being ambiguous.
|
| | |
|
| | |
|
| |
| |
| |
| | |
members of the enclosing module or its imports.
|
|/
|
|
| |
fn in fixupRevealLemma substitute the types as well.
|
|
|
|
| |
or == for equality testing.
|