[cfe-dev] Parsing VCC annotations with clang

[Florian Merz]

Hey everyone,

I'd like to work with VCC [1] annotations and clang.

This is an example for a functional contract specified in VCC's annotation 
language:

int min(int a, int b)
  _(requires \true)
  _(ensures \result <= a && \result <= b)
{
  if (a <= b)
  return a;
  else return b;
}

This is an example for object invariants specified in VCC's annotation 
language:

#define SSTR_MAXLEN 100
typedef struct SafeString {
  unsigned len;
  char content[SSTR_MAXLEN + 1];
  _(invariant \this−>len <= SSTR_MAXLEN)
  _(invariant content[len] == ’\0’)
} SafeString;


What would be necessary to make clang able to parse VCC [1] annotations like 
_(requires ...), _(ensures ...) and _(invariant)  in the example above. I'd 
like to be able to turn these into run time checks for these properties.

Best regards,
 Florian


[1] http://vcc.codeplex.com/