| Commit message (Collapse) | Author | Age |
|
|
|
| |
Visual Studio
|
|
|
|
| |
fixed minor bug in Chalice grammar
|
|
|
|
| |
sequences (for both Dafny and Chalice). This in turn fixes issue 5876.
|
| |
|
| |
|
|
|
|
| |
LHS's of CALL and RECEIVE statements (as was already done for FORK statements).
|
| |
|
|
|
|
| |
- CopyLessMessagePassing-with-ack2.chalice verifies (i.e. separate channel for acknowledgements)
|
| |
|
|
|
|
| |
(todo: we should really support sending debit over channel to allow sending with acknowledgements)
|
|
|
|
| |
- 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
|
| |
|
| |
|
|
|