| 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.
|
| |
|
|
| |
option is activated by /lazyInline:2. The original method is activated by /lazyInline: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.
|
| |
|
|
| |
changed liveVarsBefore from Boogie.Set to Generics.Set
|
| |
|
|
| |
expressions; they might not yet fully work for polymorphic maps.
|
| |
|
|
|
|
|
| |
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
|
| | |
|
| | |
|
| |
|
|
|
| |
* SscBoogie: changed default setting for /modifiesOnLoop
(we really should move this SscBoogie-specific code to the Spec# codeplex)
|
| | |
|
| |
|
mikebarnett