In some situations, inlining of fields of structured type is desirable in situations where vcc does not do it automatically, e.g., named fields are never automatically inlined.

In these situations, adding a vcc(inline) annotation to the field will cause the field to be inlined. For example:

include <vcc.h>

struct S {
  int a;
  int b;
};

struct T {
  vcc(inline) struct S s1;
  struct S s2;
  invariant(set_eq(owns(this), SET(&S2)))
};


Here, the field s1 in T is inlined, causing T to behave essentially as if it was declared like this:

struct T {
  int s1_a;
  int s1_b;
  struct S s2;
  invariant(set_eq(owns(this), SET(&S2)))
};


This means that the fields s1.a and s2.b are now in the span of T. They can no longer be owned independently of their parent.

With restrictions, the field s1 can still be used. But note that for a value t of type T, &t.s1 is of type int * and no longer struct S *. This makes it impossible to pass &t.s1 to functions that expect a typed struct S * argument. t.s1 can be passed as a value of struct S though.

Inlining of fields is particularly useful when types have many fields of small types and these types have no invariants attached.

Last edited Nov 13, 2009 at 12:03 PM by stobies, version 3

Comments

No comments yet.