| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
previously was an alternative syntax
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
* 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
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | | |
equality. Now each struct type has a default constructor that sets all of its
fields to zero-equivalent values.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
to UpdateStmt, automatically infer ghosts when local variables are introduced with a call RHS
|
| | | |
| | |
| | |
| | |
| | |
| | | |
parsing as the old VarDecl's with RHS's
To-do: automatically make some variables introduce ghost variables, depending on RHS of initial assignment
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
* 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
|
| | | |\
| | |/
| |/| |
|
| | | |
| | |
| | |
| | | |
Boogie.
|
| | | |
| | |
| | |
| | | |
allow for a return of CallRhs
|
| | | |
| | |
| | |
| | | |
soon, methods), and test cases for new name resolution rules
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* 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)
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
ICreateObjectInstance.
|
| | |\ \ |
|
| | | | |
| | | |
| | | |
| | | | |
expressions/statements
|
| | | |\ \ |
|
| | | |/ /
| |/| | |
|
| | |/ /
|/| | |
|
| | |\ \
| |/ /
|/| | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
Added a couple more stubs
|
| | | | |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
not a procedure call for calls to the method.
Use the Location (full path) instead of just the file name for source locations.
|
| | |\ \ \ |
|
| |/ / / / |
|
| | |/ / |
|
| | |\ \
| |/ /
|/| | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
added function $IsCanonicalBoolBox
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\ \ \ |
|
| |\ \ \ \
| | |/ /
| |/| | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Normalize method bodies so anonymous delegates are gone.
Some attempts at simplifying.
New regression output.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
assembly than the one under translation.
Normalize method bodies so anonymous delegates do not appear, but instead
show up as the nested classes/methods that implement them.
Beginning of some simplfication for nested expressions.
|
| | |\ \ \ |
|
Rustan Leino
Mike Barnett
Jason Koenig
Unknown
Unknown
qadeer