| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
./AbsHoudini/
./doomed/
./z3api/
./test17/
because their conversion to lit incomplete.
|
| |
|
|
| |
spaces.
|
| |
|
|
|
|
| |
we now require the OutputCheck tool. The lit.site.cfg file has
been taught to require that this tool is in the user's PATH
before testing starts.
|
| |
|
|
| |
This appears to fix a small deficiency in the original recursive implementation, so now a larger number of empty blocks are removed. As a result, various tests produce slightly different counterexamples and have been updated to reflect this. Also, default VC generation strategy has been changed to DAGIterative, to avoid stack overflow problems.
|
| |
|
|
| |
added more regressions
|
| |
|
|
| |
Added a regression
|
| |
|
|
| |
og and linear creates some rearrangement of blocks
|
| |
|
|
| |
pretty printing to always reflect when a function body is inlined
|
| | |
|
| |
|
|
|
|
|
|
|
| |
division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';
Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
|
| | |
|
| |
|
|
| |
operator when negating <, <=, >=, or >
|
| |
|
|
| |
small clean up in the inlining implementation
|
| | |
|
| |
|
|
|
|
| |
provides a non-negative number then that number is used to inline
procedures not annotated by {:inline n} attribute.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
* Added internal support for multi-dimensional arrays (but not all surface syntax is there yet)
* Removed unused variables from Dafny.atg
Boogie and Dafny:
* Improved error message for postcondition violations
|
| |
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| | |
|
| | |
|
| |
|
shuvendu
Dan Liew
Unknown
Rustan Leino
Peter Collingbourne
qadeer
Michal Moskal