| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
the version information.
|
| |
|
|
| |
unnecessary one.
|
| |
|
|
| |
version
|
| |
|
|
| |
ported C# version
|
| |
|
|
| |
"/liveVariableAnalysis:2"
|
| |
|
|
| |
inlining algorithm.
|
| | |
|
| |
|
|
| |
/stratifiedInline:1.
|
| | |
|
| |
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
/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.
|
| |
|
|
|
|
|
|
|
|
|
| |
* 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
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
Test/doomed/doomdebug.bpl
|
| |
|
|
| |
theorem prover calls (See useCE in notdoomed.bpl).
|
| |
|
|
| |
/proverWarning switch).
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
statements and writes them the stdout. Line numbers are only displayed for bpl input.
|
| | |
|
| |
|
|
|
|
| |
added first test cases for doomed (including the ones from smoke)
minor bug fixes
minor speed-ups
|
| | |
|
| |
|
|
|
| |
* 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.
|
| | |
|
| |
|
|
| |
stdout/stderr
|
| |
|
|
| |
bitvector operations
|
| | |
|
| |
|
|
| |
start block. Now it does. After the remove-empty-blocks optimization, the only possibly empty block is the start block. That is, the optimization does not change the name of the start block.
|
| |
|
mikebarnett