| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
|
| |
* Modifies clause checking is now done with each update, instead of at the end of the method. Not only does this improve error messages, but on some examples, it gives a dramatic speed-up (2x) in proving time.
* bugfix: range expressions of foreach statements were previously ignored during Translation
|
| |
|
|
| |
passive form.
|
| |
|
|
| |
translation of free variables of lambda expressions.
|
| |
|
|
|
|
| |
* Enforce ghost vs. non-ghost separation
* Allow ghost parameters and ghost locals
* Functions are ghost, but allow the non-ghost "function method"
|
| |
|
|
| |
that every datatype has some value.
|
| |
|
|
|
| |
* Added "decreases" clauses to methods.
* Interpret the filename stdin.dfy as an indication to read the program from standard input.
|
| |
|
|
| |
"call forall". Fixed printing of these attributes to print all attributes.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
* 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
|
| |
|
|
| |
changed liveVarsBefore from Boogie.Set to Generics.Set
|
| | |
|
| |
|
|
| |
expressions; they might not yet fully work for polymorphic maps.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
The functionality is currently broken.
* Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it)
* Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods
|
| |
|
|
|
|
|
| |
linear procedure call
2. Inlining requires two fields OriginalBlocks and OriginalLocVars in Implementation. These are set just before inlining is called and now I reset them to null afterwards to help garbage collection.
3. Clear live variables right after passification again to help garbage collection.
|
| |
|
|
| |
Controlled by the option /coalesceBlocks (default is to perform the optimization).
|
| |
|
|
| |
generation. This reduces the chances of Boogie causing a stack overflow.
|
| |
|
|
|
|
| |
* 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
|
| | |
|
| |
|
|
|
|
| |
2. Hoisted the call to inlining into BoogieDriver.ssc
3. Implemented a simple dead variable elimination
4. Perform inlining only for those procedures whose verification is not skipped
|
| | |
|
| | |
|
| |
|
|
| |
information
|
| |
|
|
| |
by explorer
|
| | |
|
| |
|
|
|
|
|
|
| |
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
|
| |
|
|
| |
result types of maps are declared before the type of the map itself.
|
| |
|
|
| |
used only in conjunction with /monomorphize. When enabled, this switch uses the native Z3 array theory rather than the Select-Update axioms.
|
| |
|
|
|
|
|
| |
* Allow (and currently ignore) "ghost" modifier.
* Fixed bug in boxing.
* Check for div-by-zero error for modulo operator.
* Improved emacs and latex modes.
|
| |
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
| |
print _all_ the attributes of an assert this time
add simpletypes to the visitor
|
| | |
|
| |
|
|
| |
/proverWarning switch).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
rustanleino