summaryrefslogtreecommitdiff
path: root/Source/Core/CommandLineOptions.ssc
Commit message (Collapse)AuthorAge
* Remove -z3DebugTraces and -z3Mam options (no longer working). Rename the ↵Gravatar MichalMoskal2010-08-06
| | | | -z3bv option to Z3-specific -proverOpt:OPTIMIZE_FOR_BV=true. Start with the prover-specific help (still needs changes in the yet-unconverted part).
* Boogie: added /z3bv option that overrides the current setting of Z3 options ↵Gravatar stobies2010-08-06
| | | | for better performance on VCs that are heavy on bitvector arithmetic
* Remove support for Z3 V1 and clean up parameter processing code for Z3Gravatar stobies2010-08-06
| | | | svn-ignoring some build artifacts
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
* Boogie: Added interprocedural live variable analysis. Flag to turn it on: ↵Gravatar akashlal2010-07-19
| | | | "/liveVariableAnalysis:2"
* /stratifiedInline:n eagerly inlines n times before calling the stratified ↵Gravatar akashlal2010-07-10
| | | | inlining algorithm.
* Boogie: Added stratified inlining. It is enabled using the flag ↵Gravatar akashlal2010-07-07
| | | | /stratifiedInline:1.
* Dafny:Gravatar rustanleino2010-05-06
| | | | | * Recoded frame axioms to be more goal directed * Added Main test driver to Test/VSI-Benchmarks/b2.dfy
* Dafny:Gravatar rustanleino2010-05-06
| | | | | | | | * 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
* Added another option for lazy inlining based on macro expansion. This ↵Gravatar qadeer2010-05-03
| | | | option is activated by /lazyInline:2. The original method is activated by /lazyInline:1.
* 1. Fixed lazy inlining implementation so that inlined procedures use live ↵Gravatar qadeer2010-04-30
| | | | | | variable analysis as well 2. Separeted model printing from the lazy inlining option
* 1. Fixed an off-by-one error in parsing array partitions in Z3 modelsGravatar qadeer2010-04-19
| | | | | 2. Added code for printing array partitions 3. Set UseAbstractInterpretation=false in case lazy inlining is being used
* First cut of lazy inlining. The option can be turned on by the flag ↵Gravatar qadeer2010-04-17
| | | | /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.
* Dafny: Added definedness checks for all statements (previously, some were ↵Gravatar rustanleino2010-03-13
| | | | | | missing) Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting
* Boogie:Gravatar rustanleino2010-02-20
| | | | | | | | | | | * 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
* added an option /doModSetAnalysis specially for ZvonimirGravatar qadeer2010-02-20
| | | | changed liveVarsBefore from Boogie.Set to Generics.Set
* Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda ↵Gravatar MichalMoskal2010-02-19
| | | | expressions; they might not yet fully work for polymorphic maps.
* * Added "deprecated" comment in help message about /interprocInfer switch. ↵Gravatar rustanleino2010-02-18
| | | | | | | 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
* Implemented block coalescing invoked right after type checking.Gravatar qadeer2010-02-16
| | | | Controlled by the option /coalesceBlocks (default is to perform the optimization).
* (no commit message)Gravatar qadeer2010-02-12
|
* Boogie: /useArrayTheory currently implies /monomorphizeGravatar rustanleino2010-02-09
|
* Use reflection to read version string from assembly when displaying logo ↵Gravatar stobies2010-02-08
| | | | information
* Fixed the implementation of inlining to deal with inlining depth properly.Gravatar qadeer2010-01-30
|
* Added experimental feature /DoomDebug. Can be test using ↵Gravatar schaef2010-01-28
| | | | Test/doomed/doomdebug.bpl
* Implemented the command line switch /useArrayTheory. This switch should be ↵Gravatar qadeer2010-01-21
| | | | used only in conjunction with /monomorphize. When enabled, this switch uses the native Z3 array theory rather than the Select-Update axioms.
* Added /z3lets switch, which governs which kinds of LET expressions are sent ↵Gravatar rustanleino2009-10-04
| | | | 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.
* Added /z3multipleErrors flag for generation of multiple counterexamples per ↵Gravatar mkawa2009-09-23
| | | | assert (switches off z3's /@ flag).
* * Boogie and Dafny: added /cev:<file> optionGravatar rustanleino2009-09-15
| | | | | * SscBoogie: changed default setting for /modifiesOnLoop (we really should move this SscBoogie-specific code to the Spec# codeplex)
* Dafny:Gravatar rustanleino2009-09-14
| | | | | | | | * 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.
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-05 04:58:08 +0000