summaryrefslogtreecommitdiff
path: root/Source/VCExpr/TypeErasurePremisses.cs
Commit message (Collapse)AuthorAge
* Boogie: use (WEIGHT 0) with the select-of-store axiomsGravatar Rustan Leino2011-06-29
|
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵Gravatar mikebarnett2011-03-10
| | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
* Boogie:Gravatar rustanleino2010-10-12
| | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
|
* Boogie: Removed and completed a task commentGravatar tabarbe2010-08-19
|
* 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