summaryrefslogtreecommitdiff
path: root/Source/VCExpr/TypeErasure.cs
Commit message (Expand)AuthorAge
* Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
* Modified translation so that z3 runs with type checking for simple binary ope...Gravatar Checkmate502015-10-14
* Modified internal abstract float representation to allow user-defined mantiss...Gravatar Dietrich2015-07-13
* integrated the named float type to act as a real in boogieGravatar Dietrich2015-05-04
* more work on reducing call stack consumptionGravatar qadeer2014-12-18
* Avoid another potential data race.Gravatar wuestholz2013-07-23
* Resolved some issues with data races.Gravatar wuestholz2013-07-23
* Did some refactoring.Gravatar wuestholz2013-07-23
* Did some refactoring.Gravatar wuestholz2013-07-23
* Use 'All' and 'Any' instead of 'Contract.ForAll' and 'Contract.Exists' in cod...Gravatar wuestholz2013-07-22
* All ...Seq classes now goneGravatar Ally Donaldson2013-07-22
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
* More refactoringGravatar Ally Donaldson2013-07-22
* Refactoring of TypeVariableSeqGravatar Ally Donaldson2013-07-22
* Changed Has method of PureSequence to Contains to make refactoring easier.Gravatar Ally Donaldson2013-07-22
* Refactoring of VariableSeq and TypeSeqGravatar Ally Donaldson2013-07-22
* Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
* Boogie: use (WEIGHT 0) with the select-of-store axiomsGravatar Rustan Leino2011-06-29
* Dafny: compile quantifiersGravatar rustanleino2011-03-26
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic...Gravatar mikebarnett2011-03-10
* Fix contracts so runtime checking can be turned on.Gravatar mikebarnett2011-03-07
* Boogie:Gravatar rustanleino2010-10-12
* Boogie: Removed some errors with code contracts (commenting out doubly-inheri...Gravatar tabarbe2010-08-27
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
* Make /typeEncoding:m work with arraysGravatar MichalMoskal2010-08-18
* Boogie: Committing new source code for VCExprGravatar tabarbe2010-08-13
* Boogie: Renaming VCExpr sources in preparation for port commitGravatar tabarbe2010-08-13