| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
| |
* Bug fix: Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case)
* Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants. Previously, the only option was to instrument at the beginning and end of every basic block. The new option, which is now the default, is to instrument only at the beginning of loop heads.
* Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized
* Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1
Boogie refactoring:
* Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand
* Cleaned up some parsing of command-line options
|
| |
|
|
| |
Controlled by the option /coalesceBlocks (default is to perform the optimization).
|
| | |
|
| |
|
|
|
|
|
|
| |
pretty-printer use ":" not "returns".
Allow foo(x,y,z:int,p,q:ptr) kind of syntax in function definitions.
Consequently foo(int,y:bool) is no longer allowed.
Update the testsuite to match that.
|
| |
|
|
|
|
| |
StandardVisitor while visiting commands).
This solves Issue #6266.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
and seq.
Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43).
Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed.
Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy.
Added a space in the pretty printing of Boogie coercion expressions.
|
| |
|
|
| |
This solves issue 5742, as reported in the MSR Boogie Issue Tracker on Codeplex.
|
| | |
|
| |
|
|
| |
are run.
|
| | |
|
| | |
|
| |
|
rustanleino