If you use a datatype that contains an array as one of its elements, DafnyCC can lose track of the fact that the array is allocated. This will lead to problems because most methods guarantee that they don't affect allocated parts of the heap (other than ones they explicitly modify). So if you call a method, DafnyCC may think that arrays sitting around in datatypes could have gotten modified by that method. The fix for this is to copy the array reference into a real (non-ghost variable). For instance:
var da_ref := d.a; // copy array reference d.a so DafnyCC inserts a reminder here that d.a is allocated

The places to do this are: (1) at the beginning of a method, for every array in a datatype passed as a parameter, and (2) after calling a method, for every array in a datatype returned by that method.

An entirely separate issue related to arrays in datatypes is as follows. DafnyCC needs to know whether a function (not a method) depends on the heap. Its heuristic for this is to see if any of the parameters are arrays. So that means that if it has no array parameters, but one of its parameters is a datatype that includes an array, the heuristic will fail. For this reason, you have to put the directive {:heap} on the function if it accesses the heap but doesn't have any array parameters. If you don't do this, you'll probably get errors that talk about $absMem; this is a good sign that you need the {:heap} directive.

Yet another issue is with opaque functions/predicates that operate on datatypes that contain arrays. When you call another procedure, it typically ensures that old locations in the heap remain the same, but because your function takes the entire heap as an argument, and it's opaque, Boogie can't tell that this implies the function still holds. You can call reveal_func(), but presumably you hid it for a reason. One solution is to, when you need to prove func holds, is to do:
	calc ==> {
		{ reveal_func(); }

Last edited Oct 15, 2014 at 12:11 AM by howell, version 1


No comments yet.