| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
* 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)
|
|
|
|
| |
specified
|
|
|
|
|
|
|
| |
* 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)
|
|
|
|
|
|
| |
.dfy file; duh!)
Chalice tests: removed machine-specific path from test.bat (replacing the file reference with just 'scala', which in some ways is machine-specific too)
|
|
|
|
|
|
|
| |
}'. Think of the new brackets as atomicity brackets (see PetersonsAlgorithm.chalice)
Chalice: Added Peterson's algorithm to test suite (safety properties only)
VS 2010 integration: Updated Chalice and Dafny modes, added keyword highlighting for a new Boogie mode
|
|
|
|
| |
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.
|
|
|
|
| |
LHS's of CALL and RECEIVE statements (as was already done for FORK statements).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| |
|
|
|