| Commit message (Collapse) | Author | Age |
... | |
| |
| |
| |
| | |
currently unused in the test suite)
|
| |
| |
| |
| | |
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).
|
| | |
| | |
| | |
| | |
| | | |
Window's batch doesn't recognize ";" as a command separator; lit has a
workaround for that, bu it's just as simple to do the right thing on our side.
|
| |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
runTests.py reads lit-style annotations, so we will be able to retain lit
compatibility. This new framework adds:
* Precise timings
* Proper support for interrupting using Ctrl+C
* Much better reporting (including tracking of error codes, and merging
of successive reports for performance tracking)
* No dependency on lit, OutputCheck, or Diff
* Pretty colors!
|
|/ |
|
| |
|
|
|
|
| |
explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations.
|
|\ |
|
| | |
|
| | |
|
| |
| |
| |
| | |
need for Total
|
|\| |
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|