Counting claims

By default, when you have a claim on o, you get that ref_cnt(o) >= 1. However, if you have two different claims on o, you would sometimes also like to know that ref_cnt(o) >= 2. You can make VCC infer that by explicitly asserting account_claim(c1, o) && account_claim(c2, o) where c1 and c2 are your claims. However, you will get the desired ref_cnt(o) property only when you also know c1 != c2. See the example below:

#include <vcc.h>
struct vcc(claimable) A { int dummy; };

void foo(struct A *a claimp(c1) claimp(c2) claimp(c3))
  requires(c1 != c2 && c1 != c3 && c2 != c3)
  requires(wrapped(c1) && claims_obj(c1, a))
  requires(wrapped(c2) && claims_obj(c2, a))
  requires(wrapped(c3) && claims_obj(c3, a))
{
  assert(account_claim(c1, a));
  assert(account_claim(c2, a));
  assert(account_claim(c3, a));
  assert(ref_cnt(a) >= 3);
}

As you can see it works for arbitrary number of claims.