Record Types

VCC allows the specification of record ghost types. Those types are similar to C struct types, but they are not layed-out in memory and can be translated more efficiently. Record types come with a value syntax that allows to specify field updates more concisely.

Record types are marked with the vcc(record) attribute. VCC supports the specification of record values using the field-qualified notation as in (struct S) { .a = 1, .b = 2 } , such values can also be used outside of initialization context.

Moreover, VCC supports field updates of the form s0 / { .a = 10 } , where the / operator can be read as 'where'; multiple fields can be updated at once.

Finally, record values can be compared using the C equality operator ==.

#include "vcc.h"

struct vcc(record) S {
  int a;
  int b;
};

spec(struct S foo(struct S s0) 
  ensures(result == s0 / { .a = 10 })
{
  return s0 / { .a = 10 };
}
)

void bar() {
  spec(struct S s;)
  spec(s = (struct S) { .a = 1, .b = 2 };)
  spec(s = foo(s);)
  assert(s.a == 10);
  assert(s.b == 2);
}

Updates like r.a.b = 7; are automatically translated to r = r / { .a = ( r.a / { .b = 7 } ) };.

Restrictions

Record types can only contain fields of primitive type or other record types. When a union is marked as a record, it must be flattened using the backing_member mechanism.

Records are not objects and therefore cannot have invariants.

Records cannot contain arrays, but maps are allowed.

Maps from record types are currently not supported (but see Maps from records with primitive fields).