It is a common practice to return multiple values from a function by means of the caller passing in a location, where the result should be stored. This is commonly referred to as output parameters. Sometimes the value stored in the return location at the call-site is also used, this scenario is called by-ref parameter.

A typical example looks like this:

int allocate_thing(int param, struct Thing **res)
  ensures(result == 0 ==> is_fresh(*res) && mutable(*res));

The crucial annotation is out_param(res). It is defined (in vccp.h) as:

#define out_param(p) \
  writes(p) \
  maintains(mutable(p) && is_object_root(p))

where the is_object_root(p) says that p is a top-level allocated object. This is true if p is address of a local. If p could also be address of a field of a structure, then the second form of annotation weak_out_param(p) should be used:

#define weak_out_param(p) \
  writes(p) \
  ensures(mutable(p) && unchanged(emb(p)))

The advantage of out_param(p) is that in the implementation of allocate_thing(...) you won’t have to worry about p aliasing fields of structs, and the disadvantage is that you cannot pass fields of structs as p.

Last edited Nov 13, 2009 at 12:05 PM by stobies, version 5


No comments yet.