| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
| |
are inherited
from the overridden method and Code Contracts will copy those preconditions to make sure
the right run-time checking happens; when Code Contracts finds preconditions on overrides,
it emits warnings).
|
| |
|
|
| |
the auto-triggers can be computed for ForallStmt.
|
| |
|
|
| |
This fixes a bug that affected Monad.dfy
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
This allows it to report the source of the error, giving better feedback to the
user about which precondition to a function failed to hold, for example.
|
| |
|
|
|
|
|
|
|
| |
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.
|
qunyanm
Clément Pit--Claudel