| Commit message (Collapse) | Author | Age |
|
|
|
| |
problems.
|
| |
|
| |
|
|
|
|
|
| |
Dafny: Don't display "alloc" field in BVD
Chalice: Fixed error-message parsing error in VS mode
|
|
|
|
| |
Distinguish warnings/errors in Chalice.
|
| |
|
|
|
|
| |
positions were negative
|
|
|
|
| |
be easily extensible.
|
|
|
|
|
|
|
| |
* 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)
|
|
|
|
|
|
|
| |
}'. 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
|
|
install binaries" link from the boogie.codeplex.com home page.
|