| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
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.
|
|
|
|
| |
bitvector operations
|
| |
|
|
|
|
| |
and not just the LKG.
|