| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
static field and not initialized correctly. Make it an instance field instead.
|
| |
|
|
| |
context and less in an assert.
|
| |
|
|
| |
on context.
|
| |
|
|
|
| |
derived these predicates. More things can now be verified (including the
problem reported in Issue #49).
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
- 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
|
| |/ |
|
| |
|
|
| |
function is invoked inside an "Old" expression.
|
| |
|
|
| |
as int instead of bool.
|
| |
|
|
| |
boogie function calls with "Lit" function.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
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) ]]
|
| |\ |
|
| | | |
|
| |/
|
|
| |
the auto-triggers can be computed for ForallStmt.
|
| | |
|
| |
|
|
| |
function and connect with Apply1 of the function.
|
| | |
|
| | |
|
| |
|
|
| |
protected predicated in cross-module calls) like in other places.
|
| | |
|
| |
|
|
|
|
|
| |
existential if guards.
Fixed bugs in ghost checks involving comprehensions and attributes.
Added SubstituteBoundedPool method.
|
| |
|
|
| |
of "if" statements.
|
| |
|
|
| |
ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly.
|
| |
|
|
| |
locations.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
The logic about split quantifiers is that Boogie (and z3) should never realize
that there was an unsplit quantifier. The WF check code does not produce a
quantifier, at least in it's checking part; thus, it should use original
quantifier. This fixes a problem in VerifyThis2015/Problem2.dfy with a null
check, and a problem spotted by Chris, made into a test case saved in
triggers/wf-checks-use-the-original-quantifier.dfy. The issue boiled down to
being able to verify (forall x :: x != null && x.a == 0).
Of course, the assumption that WF checks produce for a quantifier is a
quantifier, so it uses the split expression.
|
| | |
|
| |\ |
|
| | |\ |
|
| | | | |
|
| | |/
|/|
| |
| | |
merge
|
| | | |
|
| |\|
| |
| |
| |
| | |
Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This requires rewriting the parts of the AST that contain these quantifiers. We
unfortunately don't have facilities to do such rewrites at the moment (and there
are loops in the AST, so it would be hard to write such a facility). As a
workaround, this commit introduces a field in quantifier expressions,
SplitQuantifiers. Code that manipulate triggers is expected to look for this
field, and ignore the other fields if that one is found.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Implementing loop detection between multiple triggers is much harder, as it
seems to require walking an exponentially sized graph. Self-loop detection is
still a net gain compared to the current situation: we used to not detect loops
in large quantifiers; not we break these apart, suppress the loops where we can
in the smaller parts, and report the ones that we can't suppress. It could be
that the broken-up quantifiers are mutually recursive, but these cases would
have already led to a loop in the past.
|
| | |
| |
| |
| | |
This new version will include a cleaner pipeline, and trigger splitting.
|
| | |
| |
| |
| |
| | |
The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.
|
| | | |
|
| |/
|
|
|
| |
Generate warnings for malformed :induction arguments.
Removed the functionality that allowed induction on 'this'.
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| | |
There now is one main entry point for reporting errors, warnings, or
information. Next step is to make the VS extension use that.
|
| |/
|
|
| |
Signed-off-by: Clement Pit--Claudel <clement.pitclaudel@live.com>
|
| |
|
|
|
|
|
|
|
| |
The function IgnoreFuel in UnfoldingPerformance.dfy used to be lit-wrapped. It
shouldn't be, because its reads clause is non-empty. This is not a soundness
bug, but fixing it improves performance in cases where a function call would be
incorrectly unrolled.
Test case written by Rustan.
|
| | |
|
| | |
|
| |\
| |
| |
| |
| | |
This contains trigger related things under the autoTriggers flag (disabled by
default), and some bug-fixes and cleanups that are already enabled.
|
qunyanm
Michael Lowell Roberts
Clément Pit--Claudel