physical vs. specification pointers

May 31, 2010 at 7:40 PM
Edited May 31, 2010 at 7:44 PM
Hi all,

The documentation about specification pointers ("Pointers to specification memory") contains the following sentence:

The address of a specification field, variable, or parameter is implicitly of spec pointer type, so are the addresses of non-spec fields pointed to from via a spec pointer.

I doubt that this is always the right thing. Or how would one proceed in the following example?

  #include "vcc.h"
  struct List;
  struct Node
    struct Node* next;
    spec(struct List* list;)
    spec(bool initialized;)
    invariant(initialized ==> next == &list->nil)
  struct List
    struct Node nil;
    struct Node* first;

Since "list" is a specification field of "Node", the pointer "&list->nil" is of type "Node^", whereas the "next" field is of type "Node*". Thus, the equality in the invariant is not type-correct. With the above sentence of the documentation, there should be no way around this issue. Nevertheless, I'd like to specify exactly such a property. How could that be done?

Thanks, Sascha

Jun 1, 2010 at 6:01 AM

Probably, the wording is somewhat ambiguous - here is what is meant:

  • a spec field of an object on the heap is always in spec memory
  • a non-spec field of an object in spec memory is also in spec memory
  • spec parameters, locals, and globals, should their pointer be taken, reside in spe memory

If a spec field is of pointer type, is will either point to physical memory ('*') or to spec memory ('^')

In your example, since both next and list are defined using the '*' operator, both point to physical memory. If this is not the behavior that you are seeing, then there is a bug in the compiler.


Jun 1, 2010 at 6:07 AM

Yes, this seems to be a bug - we get "error VC0006: Operator '==' cannot be applied to operands of type 'Node*' and 'Node^'." for the invariant... If "list" is not declared as spec, the problem goes away.

Best, Mark


Jun 9, 2010 at 8:15 AM

I have recently comitted a change that fixes this problem - thanks for pointing this out.