summaryrefslogtreecommitdiff
path: root/Source/VCExpr
Commit message (Collapse)AuthorAge
* Added version.cs as link to those projects that were missing itGravatar stobies2010-12-06
| | | | Select 4.0 client profile on all projects
* Factored out the ParserHelper class into a separate project and updated the ↵Gravatar wuestholz2010-12-02
| | | | | | files generated by Coco/R. This was done to support sharing of the Coco/R .frame files with Spec#.
* Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.slnGravatar qadeer2010-12-01
|
* Ported all projects to .NET Framework 4.0 in both Boogie.sln and Dafny.sln. ↵Gravatar qadeer2010-11-27
| | | | Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
* Boogie:Gravatar rustanleino2010-10-12
| | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
* Update to VS2010.Gravatar MichalMoskal2010-10-07
|
* created a new build target called z3apidebug.Gravatar qadeer2010-08-29
| | | | | only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver.
* Boogie: Commented out all occurences of repeated inherited contracts - makes ↵Gravatar tabarbe2010-08-27
| | | | fewer error messages when compiling with runtime checking on.
* Boogie: Removed some errors with code contracts (commenting out ↵Gravatar tabarbe2010-08-27
| | | | doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
* Boogie: Removed an incorrect Ensures clause on a void method.Gravatar tabarbe2010-08-27
|
* Boogie: Changed the cce classes into one separate project, which every other ↵Gravatar tabarbe2010-08-27
| | | | project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
* Boogie: Basetypes port 3/3: Committing changed referencesGravatar tabarbe2010-08-27
| | | | Z3api.csproj shouldn't get in the way this time 'round.
* minor errorGravatar qadeer2010-08-27
|
* Boogie: Graph port 3/3: Committing changed references; also, adding back cce ↵Gravatar tabarbe2010-08-27
| | | | files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
* Boogie: AIFramework port part 3/3: Committing reference changes, edit to ↵Gravatar tabarbe2010-08-26
| | | | Core to jive with recent changes made to the cce class.
* Disabled an expensive contract check. Instead, only check things that are ↵Gravatar akashlal2010-08-23
| | | | actually used.
* Boogie: Committing changed referencesGravatar tabarbe2010-08-20
|
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
|
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
|
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
|
* Boogie: Fixed a few contracts errorsGravatar tabarbe2010-08-19
|
* Boogie: Removed and completed a task commentGravatar tabarbe2010-08-19
|
* 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-11-09 09:29:39 +0000