| Commit message (Collapse) | Author | Age |
|
|
|
| |
support for VS 2010.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| | |
Boogie)
|
|/ |
|
| |
|
|\ |
|
| | |
|
| |
| |
| |
| | |
buffers).
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
compilation).
|
| |
| |
| |
| | |
statements with only ghost sub-statements to be ghost
|
| | |
|
| | |
|
| |
| |
| |
| | |
any other, later)
|
| | |
|
| | |
|
| | |
|
| | |
|
|/
|
|
|
| |
Note that the 'boogie' directory is expected to be a sibling of the
'dafny' directory.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
use the instantiated types of the predicate's type parameters. This delays the
introduction of some boxes in the translation, which for some useful examples
gives rise to better proving.
|
|
|
|
|
|
|
| |
similar
to RingBufferAuto.dfy and ExtensibleArrayAuto.dfy, respectively, so that the effect
of {:autocontracts} is more easily seen.
|
|
|
|
| |
the induction-inserted 'forall' statement had caused the heap to be advanced).
|