| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
* support multi-step refinement (convert refinement blocks into normal sequences of statements)
* added tests
|
| |
|
|
|
|
| |
* added loop transform pattern
* implemented translation of refined loops to Boogie (only assert new loop invariants)
* refactored loop target computation code (async call was not handled as maybe some other statement)
|
| |
|
|
|
|
| |
* transforms are now callable
* resolve transform specs
* implement translation for refinement blocks (correct for manipulating locals, not globals)
|
| |
|
|
|
|
|
| |
* print type checked program (use -print -noTypecheck if you want old behavior)
* refactored program context in Resolver ('errors' is kept as a ListBuffer and shared)
* added resolver for refinement blocks (no loops yet)
* pretty printer should work now for transforms
|
| | |
|
| |
|
|
| |
Scala uses structural equality for case classes); landed first piece of refinement code
|
| |
|
|
| |
statement is just like a call statement now
|
| | |
|
| | |
|
| |
|
|
| |
Chalice
|
| |
|
|
| |
recursion bits
|
| |
|
|
|
|
| |
* added quantifiers over any type (forall i: int :: i + 1 == i + 1)
* cleaned up AST transformation code; organized one transform operation that should preserve source positions -- it was very annoying to see assertions with lost source positions
* added a desugar method that simplifies Chalice AST by unrolling a few constructs -- maybe useful in the future to quickly add a syntactic sugar
|
| |
|
|
|
|
|
| |
* add sequence axiom updates from Dafny
* fix a bug in pretty printer for functions and predicates
* add a command line option for not checking termination; refactor options code to update syntax help string
* relax resolver to allow ghost state in assume statements (we don't know how to compile them in general anyways; assume false is still a special case and is compiled into assert false)
|
| |
|
|
| |
in copying resolved member in sequence accesses; added graph closure (DSW) verification example
|
| |
|
|
| |
permissions. This gets of redundancy in treating acc and rd in many places and should hopefully make permissions code more comprehensible
|
| | |
|
| |
|
|
| |
resolver, printer; translation is not yet done
|
| |
|
|
| |
Boogie since it was maskng bad job done by Translator; fixing warnings in case we ever decide to switch to newer Scala compiler
|
| |
|
|
| |
operator); cleaned up some deprecation warnings; resolved ambiguity with "unfolding ... in" expression
|
| |
|
|
| |
positions.
|
| |
|
|
| |
of the "held" field in the heap
|
| |
|
|
|
| |
* renamed keyword "maxlock" to "waitlevel"
* added -vs switch, for I/O suitable for VS integration
|
| |
|
|
| |
Visual Studio
|
| |
|
|
| |
LHS's of CALL and RECEIVE statements (as was already done for FORK statements).
|
| |
|
|
| |
- all credits must be consumed on entry to a loop by the invariant (to avoid getting the wrong maxlock)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- channel declarations
- send and receive statements
- bounds clause for new, to accommodate channels
- Added ProdConsChannel.chalice test case
- Resolve and Translate (but no Compile yet)
- Added Credits to global state in encoding (this caused changes to lots of source lines)
* Simplified meaning of maxlock==E
* Various parser improvements
* Added alternative syntax for eval statements
* Some renamings in error messages (e.g., install -> reorder)
* Added preliminary parsing for condition variables and their wait and signal operations
* Added new keywords to Chalice emacs mode
|
| | |
|
| |
|
kyessenov