summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* MergeGravatar Mike Barnett2011-05-28
|\
* | Translate assignments to parameters that are of a struct type correctly. NoteGravatar Mike Barnett2011-05-28
| | | | | | | | | | | | that this means all methods with such parameters (where the parameter is passed by value) must have free preconditions expressing that the parameters are disjoint (since we are representing structs as Ref).
| * MergeGravatar Rustan Leino2011-05-27
| |\
| * | Dafny: fixed parsing bug that prevented all expressions from occurring in ↵Gravatar Rustan Leino2011-05-27
| | | | | | | | | | | | match-case expressions
| | * MergeGravatar Rustan Leino2011-05-27
| | |\
| | * | Dafny:Gravatar Rustan Leino2011-05-27
| | | | | | | | | | | | | | | | | | | | * fixed bug in allowing ghost out-parameters of ghost methods * added test case for verifying calls of the form MyClass.M(...)
| * | | Dafny: fixed compilation bug that produced an extraneous comma in the target ↵Gravatar Rustan Leino2011-05-27
| | |/ | |/| | | | | | | code
| * | MergeGravatar Rustan Leino2011-05-27
| |\ \
| | * \ MergeGravatar Jason Koenig2011-05-27
| | |\ \ | |_|/ / |/| | |
| | * | Better VisualStudio plugin feedback.Gravatar Jason Koenig2011-05-27
| | | |
* | | | MergeGravatar Mike Barnett2011-05-27
|\ \ \ \ | | |_|/ | |/| |
* | | | Translate assignments of structs as a call to a (default) copy constructorGravatar Mike Barnett2011-05-27
| | | | | | | | | | | | | | | | that does the field-by-field copy.
| | * | MergeGravatar Rustan Leino2011-05-27
| | |\ \ | | |/ / | |/| |
| * | | Dafny: permanently changed the syntax of "datatype" declarations to what ↵Gravatar Rustan Leino2011-05-27
| | | | | | | | | | | | | | | | previously was an alternative syntax
| * | | 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
| | | | | | | | | | | | | | | | | | | | | | | | * fixed ghost/non-ghost story for breaks and returns * changed compilation/translation to always use goto's to implement Dafny's breaks * introduced "break break" statements
* | | | MergeGravatar Mike Barnett2011-05-26
|\ \ \ \ | | |_|/ | |/| |
* | | | Beginning of representing structs as values on the heap, but without objectGravatar Mike Barnett2011-05-26
| | | | | | | | | | | | | | | | | | | | equality. Now each struct type has a default constructor that sets all of its fields to zero-equivalent values.
| | | * Dafny: fixed bug in induction-tactic heuristic (should never pick values ↵Gravatar Rustan Leino2011-05-26
| | | | | | | | | | | | | | | | whose type is a type parameter)
| | | * Dafny: fixed bug (ill-formed Boogie) in translation of "foreach" for sequencesGravatar Rustan Leino2011-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 ↵Gravatar Rustan Leino2011-05-25
| | | | | | | | | | | | | | | | to UpdateStmt, automatically infer ghosts when local variables are introduced with a call RHS
| | * | Dafny: changed local "var" introductions to use new VarDeclStmt instead of ↵Gravatar Rustan Leino2011-05-24
| | | | | | | | | | | | | | | | | | | | | | | | parsing as the old VarDecl's with RHS's To-do: automatically make some variables introduce ghost variables, depending on RHS of initial assignment
| | * | Dafny:Gravatar Rustan Leino2011-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * fixed parsing problem with a block ending a block * replaced AssignStmt and "call" statements with UpdateStmt's * fixed some minor printing problems * changed implementation to check for ghost expressions in a pass separate from ResolveExpr To-dos: * compile and translate multi-assignments * handle non-identifier LHSs of call statements * change "var" statements in a similar way * tighten up parsing of LHSs to allow only things like SelectExpr * code and grammar clean-up to remove unused parts (e.g., "call" grammar productions and the "allowGhostFeatures" parameters) * include the commented-out precondition of TrAssignment * check in changes to the test suite
| * | | mergeGravatar Sam Blackshear2011-05-24
| |\ \ \ | |/ / / |/| | |
| * | | New example to demonstrate exception support that would be convenient for ↵Gravatar Sam Blackshear2011-05-24
| | | | | | | | | | | | | | | | Boogie.
| | * | Dafny: refactored code into separate method ResolveIdentifierSequence and ↵Gravatar Rustan Leino2011-05-22
| | | | | | | | | | | | | | | | allow for a return of CallRhs
| | * | Dafny: allow class names to be used when referring to static functions (and, ↵Gravatar Rustan Leino2011-05-21
| | | | | | | | | | | | | | | | soon, methods), and test cases for new name resolution rules
* | | | Created an API so that a MetadataTraverser is used to translate a set ofGravatar Mike Barnett2011-05-21
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | assemblies. This enables a translator to do whole-program analyses, such as recording the subtype relationship across all of the input. (Still need to move the delegate translation into this method.) Fixed the existing whole-program translator so it uses the base class functionality for translating the arguments to a method call. Updated the regressions.
| | * Dafny:Gravatar Rustan Leino2011-05-21
| |/ |/| | | | | | | | | | | | | | | | | * started rewriting parsing of qualified identifiers in expressions * annoyingly, had to introduce AST nodes for concrete syntax * previous syntax for invoking datatype constructors: #List.Cons(h, t) new syntax: List.Cons(h, t) or, if only one datatype has a constructor named Cons: Cons(h, t) * Removed type parameters for datatype constructors from the grammar * Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied)
* | 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
| | | | | | | | | | | | ICreateObjectInstance.
| * | MergeGravatar Rustan Leino2011-05-19
| |\ \
| * | | Dafny: let verifier, not the resolver, check for missing cases in match ↵Gravatar Rustan Leino2011-05-19
| | | | | | | | | | | | | | | | expressions/statements
| | * | 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 a couple more stubs
* | | 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
| | | | | | | | | | | | | | | | | | | | not a procedure call for calls to the method. Use the Location (full path) instead of just the file name for source locations.
| * | | MergeGravatar qadeer2011-05-17
| |\ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-18 12:56:20 +0000