| 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)
|
| |
|
|
| |
to disable)
|
| |
|
|
|
|
| |
* transforms are now callable
* resolve transform specs
* implement translation for refinement blocks (correct for manipulating locals, not globals)
|
| |
|
|
| |
Scala uses structural equality for case classes); landed first piece of refinement code
|
| |
|
|
| |
(i.e. if function app was inside old, the flag was ignored); != was not properly translated for sequences
|
| |
|
|
| |
statement is just like a call statement now
|
| | |
|
| |
|
|
| |
specified
|
| | |
|
| |
|
|
| |
Chalice
|
| |
|
|
| |
added classic sqrt refinement; assertions on acc(s[*].f) have now positions attached
|
| |
|
|
|
|
|
| |
* change syntax for range: [a..b] instead of [a:b]
* add multi-triggers to Boogie bindings
* fix unsoundness in frame axiom for functions -- whenever acc(s[*].f,...) is detected in pre-condition, a different encoding to Boogie is applied
* add limited functions to translator (disabled since Resolver is not ready yet)
|
| |
|
|
|
|
| |
* 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
|
| |
|
|
| |
(due to "implicit def")
|
| | |
|
| |
|
|
| |
(sans checking for epsilon going beyond infinity and rd(...,*) permissions)
|
| |
|
|
| |
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
|
| |
|
|
| |
permission expression; refactored Translator my moving prelude/implicits into TranslatorHelper for consistency
|
| |
|
|
| |
variable declarations and method/function formals); the clause says that every element in a sequence is either null or its dtype is the element type
|
| |
|
|
| |
Boogie since it was maskng bad job done by Translator; fixing warnings in case we ever decide to switch to newer Scala compiler
|
| |
|
|
| |
containment; refactoring and preparing to extend wild card permissions to sequences
|
| |
|
|
| |
operator); cleaned up some deprecation warnings; resolved ambiguity with "unfolding ... in" expression
|
| |
|
|
| |
expressions
|
| |
|
|
| |
is now required to list all objects whose held or rdheld field has changed since the _method_ prestate. It seems desirable to exclude objects that were not allocated in the prestate, but this feature is not implemented yet.
|
| |
|
|
| |
of the "held" field in the heap
|
| |
|
|
| |
Adapted definition of IsGoodInhaleState and an axiom.
|
| |
|
|
|
| |
* renamed keyword "maxlock" to "waitlevel"
* added -vs switch, for I/O suitable for VS integration
|
| |
|
|
| |
Patches the translation of "assert" statements, so that the meaning of "old" is preserved when the temporary copy of the heap is made for the exhale.
|
| | |
|
| |
|
|
| |
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)
|
| |
|
|
| |
some demos that use locks before explaining the global order on locks.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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