| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case).
* Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.)
* Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type.
* More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal")
* Add axioms about idempotence of set union and intersection
* The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one
* In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase
* Fixed error in translation of while(*)
|
| |
|
|
| |
rep axiom
|
| |
|
|
|
| |
Dafny: Don't display "alloc" field in BVD
Chalice: Fixed error-message parsing error in VS mode
|
| |
|
|
| |
Distinguish warnings/errors in Chalice.
|
| |
|
|
|
|
| |
constructs.
Dafny VS2010 extension: link with Dafny and use it to parse and type check
|
| | |
|
| | |
|
| |
|
|
|
|
| |
* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation)
* Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays.
* Internally, this meant adding support for built-in classes and readonly fields
|
| | |
|
| |
|
|
| |
with string literals
|
| |
|
|
| |
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)
|
| |
|
|
|
|
| |
.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
|
|
|
install binaries" link from the boogie.codeplex.com home page.
|
rustanleino