| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.
|
| |
|
|
| |
input).
|
| |
|
|
| |
-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
|
| | |
|
| |
|
|
| |
project; making Core work with the port by removing the nonnull requirements on one abstract method.
|
| | |
|
| |
|
|
| |
"/liveVariableAnalysis:2"
|
| |
|
|
| |
inlining algorithm.
|
| |
|
|
| |
/stratifiedInline:1.
|
| |
|
|
| |
'BoogiePL.Parser.Parse'.
|
| |
|
|
| |
ones.
|
| |
|
|
|
|
| |
having them in this repository because of license issues. Instead, they must be downloaded from http://boogiepartners.codeplex.com/ and then copied into the appropriate directories.
Lots of code changes to compensate for the new frame files.
|
| |
|
|
| |
LoopUnroll constructor
|
| |
|
|
| |
SCC.
|
| |
|
|
|
|
|
|
|
|
| |
* Added support for polymorphism in lambda expressions
* Little clean-up here and there
* Added 'then' keyword to emacs and latex modes
Dafny:
* Added support for fine-grained framing, using the back-tick syntax from Region Logic
* Internally, changed checking of reads clauses to use a local variable $_Frame, analogous to the $_Frame variable used in checking modifies clauses
|
| | |
|
| |
|
|
|
| |
* 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 facility for giving weights to the generated quantifiers for lazy inlining; however, left the weights at default 1.
|
| |
|
|
|
| |
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
|
| |
|
|
| |
passive form.
|
| |
|
|
| |
translation of free variables of lambda expressions.
|
| |
|
|
|
| |
* 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).
|
| | |
|
| |
|
|
|
|
| |
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
|
| | |
|
| |
|
|
| |
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.
|
akashlal