summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Dafny: let verifier, not the resolver, check for missing cases in match expre...Gravatar Rustan Leino2011-05-19
* MergeGravatar Rustan Leino2011-05-18
|\
* | Dafny: added set comprehension expressionsGravatar Rustan Leino2011-05-18
| * Fixed array constructionGravatar qadeer2011-05-17
| * added another axiomGravatar Unknown2011-05-17
| * MergeGravatar Mike Barnett2011-05-17
| |\
| * | If a method has been translated as a function, generate a function call andGravatar Mike Barnett2011-05-17
| | * MergeGravatar qadeer2011-05-17
| | |\
| | * | added spec for GetTypeGravatar qadeer2011-05-17
| |/ /
| | * Boogie build succeededGravatar CodeplexBot2011-05-17
| |/ |/|
* | MergeGravatar Rustan Leino2011-05-16
|\|
* | Dafny: Test case for sequence of boxed booleansGravatar Rustan Leino2011-05-16
* | Dafny: To help verifications involving sequences of (boxed) booleans along, a...Gravatar Rustan Leino2011-05-16
| * Fix command-line option processing.Gravatar Mike Barnett2011-05-16
| * bug fixesGravatar qadeer2011-05-16
| * Fix break.Gravatar Mike Barnett2011-05-16
| * new regression outputGravatar Mike Barnett2011-05-16
| |\
| * \ MergeGravatar Mike Barnett2011-05-16
| |\ \ | |/ / |/| |
| * | mergeGravatar Mike Barnett2011-05-16
| * | MergeGravatar Mike Barnett2011-05-16
| | * Add extern declarations to procedures.Gravatar Mike Barnett2011-05-16
| | * Mark procedures/functions as "extern" if they are defined in a differentGravatar Mike Barnett2011-05-16
* | | MergeGravatar qadeer2011-05-16
|\ \ \
* | | | convert assert to requiresGravatar qadeer2011-05-16
| |/ / |/| |
| * | Dafny: added some test cases that use natGravatar Rustan Leino2011-05-16
| * | Dafny: added optional range expressions to logical quantifiers, preparing for...Gravatar Rustan Leino2011-05-15
|/ /
* | MergeGravatar Rustan Leino2011-05-14
|\ \
* | | Dafny: fixed bug in quantifier bounds discoveryGravatar Rustan Leino2011-05-14
| * | Boogie build failedGravatar CodeplexBot2011-05-14
|/ /
* | Dafny: fixed typo in parser codeGravatar Rustan Leino2011-05-13
* | MergeGravatar Rustan Leino2011-05-13
|\ \
* | | Boogie: added features to help with modular verification. In particular, defi...Gravatar Rustan Leino2011-05-13
* | | Cleaner version of ghost loop termination example.Gravatar Unknown2011-05-13
* | | Add source file (Expression Design) for the BVD icon in case anyone ever need...Gravatar Michal Moskal2011-05-12
* | | Dafny: fixed bugs in resolution of multi-dimensional arraysGravatar Rustan Leino2011-05-12
* | | MergeGravatar Rustan Leino2011-05-12
|\ \ \
* | | | Dafny: forbid "decreases *" on ghost loopsGravatar Rustan Leino2011-05-12
| | | * MergeGravatar Mike Barnett2011-05-12
| | | |\ | | |_|/ | |/| |
| | | * Trying to fix the bound expression simplifier.Gravatar Mike Barnett2011-05-12
| * | | added examples of generics and string support needed by PoirotGravatar 10shb2011-05-12
|/ / /
* | | MergeGravatar Rustan Leino2011-05-11
|\ \ \
* | | | More files for Hg to ignoreGravatar Rustan Leino2011-05-11
| * | | first cut at handling genericsGravatar qadeer2011-05-11
| | |/ | |/|
| | * Dafny:Gravatar Rustan Leino2011-05-11
* | | MergeGravatar Rustan Leino2011-05-11
|\ \ \
* | | | Dafny: fixed compilation bugs, added @-signs in front of identifiers to avoid...Gravatar Rustan Leino2011-05-11
| |/ / |/| |
| * | Dafny: Fixed non-compiling C# code in DafnyRuntime.csGravatar Rustan Leino2011-05-11
* | | simplified the translation of assignmentsGravatar qadeer2011-05-10
* | | MergeGravatar Mike Barnett2011-05-10
|\ \ \
* | | | Oops. Last checkin did not contain the changes for the catch clause change whenGravatar Mike Barnett2011-05-10