search

mattulbrich / dive

Dafny Interactive Verification Environment (DIVE)
GNU General Public License v3.0
4 stars 0 forks source link

Incomplete boogie translation #194

Open mattulbrich opened 3 years ago

mattulbrich commented 3 years ago

The following cannot be proved by boogie:

### project:
class C { var f : int; }

### decls:
o : C
a : array<int>

### sequent:
|- o.f == o.f@$heap[a[0] := 0]

### result:
prove

The translation is incomplete since the array-index 0 may alias with C$$f in the boogie translation.