This project is read-only.

Can I assert that an object has a particular type?

Feb 9, 2011 at 8:56 PM

What I'd like to be able to do is something like this:

struct GenericHolder {

   _(ghost  \object subject ; )

};

 

struct Foo { ... } ;

struct FooHolder {

   struct GenericHolder h ;

   _(invariant h.subject hasType (Foo*) )

};

That is I'd like to be able to state that a particular object pointer has a particular type.

The draft tutorial says that, while \object is similar to void*, it contains some dynamic type information.  However, I can't find any way to access this information.

Cheers,

Theo

Feb 9, 2011 at 9:51 PM

Hi Theo,

  there is the "\is" annotation. "A \is B" assert that given pointer "A" is of type "B*":

#include "vcc.h"

struct GenericHolder {
   int a;
   _(ghost \object subject)
};
 
struct Foo {
  int b;
};

struct FooHolder {
   struct GenericHolder h;
   _(invariant \mine(&h))
   _(invariant h.subject \is struct Foo)
};

  Regards, Mark

Feb 11, 2011 at 9:06 PM

Mark:  As always, thanks a million.

 

Cheers,

Theo