| Commit message (Collapse) | Author | Age |
|
|
|
| |
-z3bv option to Z3-specific -proverOpt:OPTIMIZE_FOR_BV=true. Start with the prover-specific help (still needs changes in the yet-unconverted part).
|
|
|
|
| |
for better performance on VCs that are heavy on bitvector arithmetic
|
|
|
|
| |
svn-ignoring some build artifacts
|
| |
|
|
|
|
| |
"/liveVariableAnalysis:2"
|
|
|
|
| |
inlining algorithm.
|
|
|
|
| |
/stratifiedInline:1.
|
|
|
|
|
| |
* Recoded frame axioms to be more goal directed
* Added Main test driver to Test/VSI-Benchmarks/b2.dfy
|
|
|
|
|
|
|
|
| |
* First crack at a compiler (/compile:1 writes out.cs, if Dafny program verifies)
* Added "print" statement (to make running compiled programs more interesting)
* Changed name of default class from $default to _default
Boogie:
* Included "lambda" as a keyword in emacs and latex style files
|
|
|
|
| |
option is activated by /lazyInline:2. The original method is activated by /lazyInline:1.
|
|
|
|
|
|
| |
variable analysis as well
2. Separeted model printing from the lazy inlining option
|
|
|
|
|
| |
2. Added code for printing array partitions
3. Set UseAbstractInterpretation=false in case lazy inlining is being used
|
|
|
|
| |
/lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.
|
|
|
|
|
|
| |
missing)
Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
|
|
|
|
|
|
|
|
|
|
|
| |
* 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
|
|
|
|
| |
Controlled by the option /coalesceBlocks (default is to perform the optimization).
|
| |
|
| |
|
|
|
|
| |
information
|
| |
|
|
|
|
| |
Test/doomed/doomdebug.bpl
|
|
|
|
| |
used only in conjunction with /monomorphize. When enabled, this switch uses the native Z3 array theory rather than the Select-Update axioms.
|
|
|
|
| |
to Z3. By default, both LET TERM and LET FORMULA expressions are used. Mode /z3lets:2 uses only LET FORMULA, which works around a current Z3 issue with LET expressions and nested quantifiers.
|
|
|
|
| |
assert (switches off z3's /@ flag).
|
|
|
|
|
| |
* SscBoogie: changed default setting for /modifiesOnLoop
(we really should move this SscBoogie-specific code to the Spec# codeplex)
|
|
|
|
|
|
|
|
| |
* Added DeclType(f)==C axioms, which for each field f says which class declares it.
Boogie:
* Changed behavior of free loop invariants. Now, a free loop invariant is ignored on the checking side, just like for free requires and free ensures. The new switch /alwaysAssumeFreeLoopInvariants flag gives the previous behavior.
* NOTE: I did NOT yet make the corresponding change for loop unrolling, but it is needed.
|
|
|