| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
|
| |
* Added "decreases" clauses to methods.
* Interpret the filename stdin.dfy as an indication to read the program from standard input.
|
| |
|
|
|
|
|
|
|
|
|
| |
* 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
|
| | |
|
| |
|
|
| |
expressions; they might not yet fully work for polymorphic maps.
|
| | |
|
| |
|
|
| |
Controlled by the option /coalesceBlocks (default is to perform the optimization).
|
| | |
|
| |
|
|
|
|
| |
* Allow ghost methods (all "ghost" keywords are currently parsed and then ignored)
* Improved and made more automatic the treatment of "use" functions (a good next step would be to automatically infer which functions would make good "use" functions)
* Include preconditions in all definedness checks of function-call expressions
|
| | |
|
| |
|
|
|
|
|
|
| |
boolean-only if-then-else expressions)
Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter)
Dafny grammar changes: Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::'
Dafny: Check for division-by-zero for both '/' and '%'
|
| | |
|
| |
|
|
| |
Test/doomed/doomdebug.bpl
|
| | |
|
| |
|
|
| |
theorem prover calls (See useCE in notdoomed.bpl).
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
Change the runtest.bat to report the testname in "succeeded/failed" message, so
one can make sense of the multiple core output.
|
| |
|
|
| |
bvInt handling in Boogie
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* If no decreases clause is given, the decreases clause defaults to the set of objects denoted by the reads clause, which was the previous Dafny behavior
* Made Dafny check loops for termination by default. Previously, this was done only if the loop had a decreases clause. To indicate that a loop is to be checked only for partial correctness, Dafny now allows "decreases *".
* Allow "reads *" to say that the function may read anything at all (sound, but not very useful)
* Adjusted frame axioms of functions to speak of allocated objects more liberally; and also added antecedents about the heaps being well-formed and the parameters being allocated
* Added some previously omitted well-definedness checks.
* Fixed some bugs in the resolver that caused some type errors not to be reported
* Added some messages to go with some (previously rather opaquely reported) errors
* Fixed some test cases that previously had ordered conjuncts incorrectly to prove termination and reads checks (such checks were previously omitted)
* Beefed up Test/dafny0/SchorrWaite.dfy to use datatypes to specify that no garbage gets marked. The full-functional total-correctness verification of this Schorr-Waite method now takes about 3.2 seconds.
|
| |
|
|
|
|
| |
bodies) match expressions.
Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.
|
| | |
|
| |
|
|
|
|
| |
StandardVisitor while visiting commands).
This solves Issue #6266.
|
| | |
|
| |
|
|
| |
statements and writes them the stdout. Line numbers are only displayed for bpl input.
|
| | |
|
| |
|
|
| |
Included VSI-Benchmarks in standard tests.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
variables, if they were not already local variables.
|
| |
|
|
|
|
|
| |
"!(x in S)".
Changed Dafny test files to use the new operator.
Included the file b8.dfy into the VSI-Benchmarks test harness.
|
| |
|
|
| |
uncomment a couple of the desired loop invariants.)
|
| |
|
|
|
|
| |
added first test cases for doomed (including the ones from smoke)
minor bug fixes
minor speed-ups
|
| | |
|
| |
|
|
| |
This solves issue 5742, as reported in the MSR Boogie Issue Tracker on Codeplex.
|
| |
|
|
| |
Deleted/ignored some binaries in the Binaries directory.
|
| | |
|
| |
|
|
| |
are run.
|
| | |
|
| | |
|
| |
|
rustanleino