summaryrefslogtreecommitdiff
path: root/Source/VCExpr
Commit message (Expand)AuthorAge
* Fix some more contracts.Gravatar mikebarnett2011-03-07
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
* Add VCExprNAry.UniformArguments property to return arguments of nested And/Or...Gravatar MichalMoskal2011-02-15
* Move name-quoting (already for SMT2 not SMT1) into a seprate classGravatar MichalMoskal2011-02-15
* The TPTP backend works for some very limited examplesGravatar MichalMoskal2011-01-18
* Use a made-up name when Context.Lookup() cannot find a nameGravatar MichalMoskal2010-12-10
* Added version.cs as link to those projects that were missing itGravatar stobies2010-12-06
* Factored out the ParserHelper class into a separate project and updated the f...Gravatar wuestholz2010-12-02
* 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
* Boogie:Gravatar rustanleino2010-10-12
* Update to VS2010.Gravatar MichalMoskal2010-10-07
* created a new build target called z3apidebug.Gravatar qadeer2010-08-29
* Boogie: Commented out all occurences of repeated inherited contracts - makes ...Gravatar tabarbe2010-08-27
* Boogie: Removed some errors with code contracts (commenting out doubly-inheri...Gravatar tabarbe2010-08-27
* 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
* Boogie: Basetypes port 3/3: Committing changed referencesGravatar tabarbe2010-08-27
* minor errorGravatar qadeer2010-08-27
* Boogie: Graph port 3/3: Committing changed references; also, adding back cce ...Gravatar tabarbe2010-08-27
* Boogie: AIFramework port part 3/3: Committing reference changes, edit to Core...Gravatar tabarbe2010-08-26
* Disabled an expensive contract check. Instead, only check things that are act...Gravatar akashlal2010-08-23
* 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 (w...Gravatar MichalMoskal2010-08-18
* Change Synonym type printing to what it was, use a workaround in TypeToString...Gravatar MichalMoskal2010-08-18
* Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m us...Gravatar MichalMoskal2010-08-18
* Make /typeEncoding:m work with arraysGravatar MichalMoskal2010-08-18
* Boogie: Adding 1 more necessary source file for VCExpr, removing an unnecessa...Gravatar tabarbe2010-08-13
* 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 in...Gravatar rustanleino2010-08-10
* 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 /lazyInl...Gravatar qadeer2010-04-17
* Boogie:Gravatar rustanleino2010-02-20
* Implement if-then-else expression.Gravatar MichalMoskal2010-02-18
* * Added "deprecated" comment in help message about /interprocInfer switch. T...Gravatar rustanleino2010-02-18
* 1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a linea...Gravatar qadeer2010-02-16
* Boogie: Peephole optimization to reduce depth of formulas created during VC ...Gravatar rustanleino2010-02-15
* Implemented the command line switch /useArrayTheory. This switch should be u...Gravatar qadeer2010-01-21
* Evidently, Z3 does not like QID's to start with a digit. If a Boogie filenam...Gravatar rustanleino2009-10-14
* Added /z3lets switch, which governs which kinds of LET expressions are sent t...Gravatar rustanleino2009-10-04
* Fixed some bugs in the generation of bitvector input for Z3.Gravatar rustanleino2009-09-29
* Use type-erased result type to make decision about whether or not to include ...Gravatar rustanleino2009-09-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 22:50:36 +0000