| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\ |
|
| | | |
|
| |/ |
|
| |
|
|
| |
.cs file with the new /spillTargetCode switch
|
| | |
|
| |
|
|
| |
avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
|
| |
|
|
| |
assignments where RHS is not just an expression
|
| |
|
|
|
|
|
|
|
|
|
| |
syntax. What you previously would have written like:
c := new C;
call c.Init(x, y);
you can now write as:
c := new C.Init(x, y);
|
| |
|
|
|
|
| |
Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction
Dafny: split expressions when proving function postconditions
Boogie and BVD: updated copyright year ranges
|
| |
|
|
| |
to "function" in a test case.
|
| |
|
|
|
| |
Dafny: Don't display "alloc" field in BVD
Chalice: Fixed error-message parsing error in VS mode
|
| | |
|
| |
|
|
| |
Dafny: Simplified VSComp2010/Problem4-Queens.dfy from using an inductive ghost-method lemmas to just using an assert
|
| |
|
|
|
|
| |
* 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
|
| |
|
afd
Unknown
Rustan Leino
Unknown