| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
The issues here are mostly with induction (wrt. to trigger selection and
quantifier splitting) and with expressions like P(i, j-1) where no good choices
are available.
|
| |
|
|
|
|
| |
those heap location that hold the array elements
|
| |
|
|
|
|
|
|
| |
themselves.
Other serendipitous axiom improvements.
|
|
|
|
| |
Improved situation with (reducing bogosity of) type checking of "object".
|
|
|
|
| |
arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
with duplicate array.Length functions in generated Boogie file.
|
|
|
|
| |
updated regression tests.)
|
|
|
|
| |
assignments where RHS is not just an expression
|
|
|
|
|
|
| |
* 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
|
|
* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks
|