| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
In previous versions, it was sufficient to just pass /z3exe:/usr/bin/z3
in the dafny launcher script, but now, Dafny looks for its vendored
Z3 (which we don’t install) at runtime and prints a warning if it’s
gone. Patch that behaviour away, hardcoding /usr/bin/z3 as the Z3
binary location.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| | |
|
| |
| |
| |
| | |
Changed copyright date to include 2016.
|
| |\ |
|
| | | |
|
| | | |
|
| |/
| |
| |
| | |
wrong.
|
| | |
|
| |
| |
| |
| | |
static field and not initialized correctly. Make it an instance field instead.
|
| |\ |
|
| | |
| | |
| | |
| | | |
context and less in an assert.
|
| |/ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
error
if more than one method is so annotated. For that method, the usual restrictions
for "main" apply, but it is allowed to take ghost arguments, and it is allowed
to have preconditions. This lets the programmer add some explicit assumptions
about the outside world, modeled, for example, via ghost parameters.
|
| |
| |
| |
| |
| | |
it. Don't use pretty warning signs since we can't diff them correctly in the
test output from the test run.
|
| |
| |
| |
| |
| | |
one exported view, but no exported view is marked as default, then it is an
error.
|
| |
| |
| |
| | |
on context.
|
| | |
|
| |\ |
|
| | |
| | |
| | |
| | |
| | | |
derived these predicates. More things can now be verified (including the
problem reported in Issue #49).
|
| | | |
|
| | |
| | |
| | |
| | | |
until the editor is idle for 5 second.
|
| |/
| |
| |
| | |
declared outside the enclosing match.
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | | |
- various peephole optimizations of formulas, to generate fewer tautologies
- removed unused bound variables in CanCall quantifications (this addresses Issue #135)
- added type- and precondition-antecedent in quantified CanCall assumption for lambda expressions, thus fixing an unsoundness
|
| | |
| | |
| | |
| | | |
"case" of a match statement and match expression.
|
| | |
| | |
| | |
| | | |
of console.
|
| | | |
|
| |/ |
|
| | |
|
| |
| |
| |
| | |
function is invoked inside an "Old" expression.
|
| | |
|
| |
| |
| |
| | |
as int instead of bool.
|
| | |
|
| |\ |
|
| | |
| | |
| | |
| | | |
a class is referenced.
|
| |/ |
|
| |
| |
| |
| | |
boogie function calls with "Lit" function.
|
| |
| |
| |
| | |
as candidates for triggers.
|
| |
| |
| |
| |
| | |
the test was moved into test\dafny0\modules0.dfy so that bug125.dfy can be
verified that it was resolved to the correct types.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
For the following situation
module LibA {
// ...things declared here...
}
module LibB {
// ...things declared here...
}
module R {
import opened LibA
// ...things declared here...
}
module S refines R {
import opened LibB
// ...declared here...
}
1. If module R declares a TopLevelDecl “G”, then we should report an error if S
attempts to declare an incompatible TopLevelDecl “G”. Dafny does this already.
2. If LibA declares a TopLevelDecl “G” but R does not directly declare any
TopLevelDecl G”, then we should also issue an error for any TopLevelDecl “G”
in S. This behavior is missing in Dafny.
3. If each of LibA and LibB declares some TopLevelDecl “G”, but neither R nor S
directly declares any TopLevelDecl “G”, then no error should be issued, and
any use of “G” in S should resolve to the “G” in LibA. This behavior is missing
in Dafny.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
expression from
// CanCall[[ var b :| RHS(b,g); Body(b,g,h) ]] =
// (forall b0,b1 :: typeAntecedent ==>
// CanCall[[ RHS(b,g) ]] &&
// (RHS(b,g) ==> CanCall[[ Body(b,g,h) ]]) &&
// $let$canCall(b,g))
to
// CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] =
// $let$canCall(g) &&
// CanCall[[ Body($let$b0(g), $let$b1(g), h) ]]
|
| |
| |
| |
| |
| |
| |
| |
| | |
instantiate all it arguments, don't stop as soon as one instantiable constructor
is found. Instead, figure out all instantiable constructors and then pick the
best among these. A simple and reasonable "best" is an instantiable constructor
that requires a minimal number of already constructed type arguments, and to
break ties among these, pick the first one listed.
|
| | |
|
| |
| |
| |
| | |
module.
|