summaryrefslogtreecommitdiff
path: root/Source/VCExpr
Commit message (Collapse)AuthorAge
...
* Chase type synonyms in arguments/results of map types when generating name ↵Gravatar MichalMoskal2010-08-18
| | | | (with tE:m).
* Change Synonym type printing to what it was, use a workaround in ↵Gravatar MichalMoskal2010-08-18
| | | | TypeToString() instead. Add test for /typeEncoding:m.
* Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m ↵Gravatar MichalMoskal2010-08-18
| | | | use separate Z3 type per Boogie type
* Make /typeEncoding:m work with arraysGravatar MichalMoskal2010-08-18
|
* Boogie: Adding 1 more necessary source file for VCExpr, removing an ↵Gravatar tabarbe2010-08-13
| | | | unnecessary one
* Boogie: Committing new source code for VCExprGravatar tabarbe2010-08-13
|
* Boogie: Renaming VCExpr sources in preparation for port commitGravatar tabarbe2010-08-13
|
* Boogie: Added boolean code expressions (sans well-formedness checks on the ↵Gravatar rustanleino2010-08-10
| | | | input).
* Boogie: Fixed a few line endingsGravatar tabarbe2010-08-06
|
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
* Fixed bug in translation of select/store arguments that are BooleanGravatar qadeer2010-04-20
|
* 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.
* 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
* Implement if-then-else expression.Gravatar MichalMoskal2010-02-18
|
* * 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
* 1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a ↵Gravatar qadeer2010-02-16
| | | | | | | 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.
* Boogie: Peephole optimization to reduce depth of formulas created during VC ↵Gravatar rustanleino2010-02-15
| | | | generation. This reduces the chances of Boogie causing a stack overflow.
* 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.
* Evidently, Z3 does not like QID's to start with a digit. If a Boogie ↵Gravatar rustanleino2009-10-14
| | | | | | filename starts with a digit, don't just prepend it to a QID, but prepend another character ('_') first. This fixes issue 5278 in the Issue Tracker.
* 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.
* Fixed some bugs in the generation of bitvector input for Z3.Gravatar rustanleino2009-09-29
| | | | Deleted/ignored some binaries in the Binaries directory.
* Use type-erased result type to make decision about whether or not to include ↵Gravatar rustanleino2009-09-27
| | | | antecedent in select-of-store axioms (fixing an error in my previous check-in).
* Added antecedent to select-of-store axioms to make them sound even when ↵Gravatar rustanleino2009-09-24
| | | | triggers are ignored.
* Renaming ExtractExpr into BvExtractExpr to fit naming scheme of the other ↵Gravatar stobies2009-09-07
| | | | bitvector operations
* Sign assembliesGravatar stobies2009-08-17
|
* Made trigger more liberal for int_2_U U_2_int axiom.Gravatar rustanleino2009-07-30
|
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 13:15:32 +0000