summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* MergeGravatar Mike Barnett2011-05-27
|\
* | Translate assignments of structs as a call to a (default) copy constructorGravatar Mike Barnett2011-05-27
| * Dafny: permanently changed the syntax of "datatype" declarations to what prev...Gravatar Rustan Leino2011-05-27
| * Dafny: retired "use" statementsGravatar Rustan Leino2011-05-27
| * Dafny: added chaining operatorsGravatar Rustan Leino2011-05-27
| * MergeGravatar Rustan Leino2011-05-26
| |\ | |/ |/|
| * Dafny:Gravatar Rustan Leino2011-05-26
* | MergeGravatar Mike Barnett2011-05-26
|\ \
* | | Beginning of representing structs as values on the heap, but without objectGravatar Mike Barnett2011-05-26
| * | VisualStudio plugin now informs the user of a timeout.Gravatar Jason Koenig2011-05-26
| | * Dafny implementation: removed always-true "allowGhostFeatures" parameterGravatar Rustan Leino2011-05-26
| | * Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
| | * Dafny: cleaned up parser, moved foreach statement from AssignStmt<> parsing t...Gravatar Rustan Leino2011-05-25
| | * Dafny: changed local "var" introductions to use new VarDeclStmt instead of pa...Gravatar Rustan Leino2011-05-24
| | * Dafny:Gravatar Rustan Leino2011-05-24
| * | mergeGravatar Sam Blackshear2011-05-24
| |\ \ | |/ / |/| |
| * | New example to demonstrate exception support that would be convenient for Boo...Gravatar Sam Blackshear2011-05-24
| | * Dafny: refactored code into separate method ResolveIdentifierSequence and all...Gravatar Rustan Leino2011-05-22
| | * Dafny: allow class names to be used when referring to static functions (and, ...Gravatar Rustan Leino2011-05-21
* | | Created an API so that a MetadataTraverser is used to translate a set ofGravatar Mike Barnett2011-05-21
| | * Dafny:Gravatar Rustan Leino2011-05-21
| |/ |/|
* | Boogie build succeededGravatar CodeplexBot2011-05-20
* | Dafny: added alternative statement and alternative-loop statementGravatar Rustan Leino2011-05-19
* | MergeGravatar Mike Barnett2011-05-19
|\ \
* | | Unify translation of arguments so the same code is used for IMethodCall andGravatar Mike Barnett2011-05-19
| * | MergeGravatar Rustan Leino2011-05-19
| |\ \
| * | | Dafny: let verifier, not the resolver, check for missing cases in match expre...Gravatar Rustan Leino2011-05-19
| | * | mergeGravatar Unknown2011-05-19
| | |\ \
| | | * | close the file stream opened by the parserGravatar Unknown2011-05-19
| | |/ / | |/| |
| | * | fixed the axiom about TypeOfGravatar Unknown2011-05-18
| |/ / |/| |
| * | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-30 03:20:11 +0000