Global variables are considered to be mutable at the entry point of the program. The entry point state is characterized by the program_entry_point() function (implicitly taking state as the parameter). Therefore the usual specification on the main function of the program will look like this:

#include <vcc.h>

int g;

int main()
  writes(set_universe())
  requires(program_entry_point())
{
  g = 12;
}

After the entry point it is up to you to maintain mutability of global variables.

It is actually easy when you want to write them in a single-threaded environment:

#include <vcc.h>

int g;

void foo()
  writes(&g)
{
  g = 12;
}

This will verify, because the writes(...) annotation will implicitly assume that g is mutable. However when you want to read them, without listing them in the writes clause, you need to require them to be thread_local , with the usual problems (like them ceasing to be thread local after any call that could write something).

For more structured or multithreaded code it is advisable to use ownership to keep track of globals. One can for example introduce global ghost structures to own things:

#include <vcc.h>

typedef struct _DATA {
  int a;
  int b;
  invariant(a + b > 0)
} DATA;

typedef struct _LOCK {
    volatile int locked;
    spec(obj_t protected_obj;)
    // invariants omitted...
} LOCK;

void InitializeLock(LOCK *lock spec(obj_t protected_obj))
    writes(span(lock), protected_obj)
    requires(wrapped(protected_obj))
    ensures(wrapped(lock))
    ensures(!lock->locked)
    ensures(lock->protected_obj==protected_obj);

void Acquire(LOCK *lock claimp(c))
    always(c, closed(lock))
    ensures(wrapped(lock->protected_obj))
    ensures(is_fresh(lock->protected_obj));

void Release(LOCK *lock claimp(c))
    always(c, closed(lock))
    requires(c!=lock->protected_obj)
    requires(wrapped(lock->protected_obj))
    writes(lock->protected_obj);

LOCK DataLock;
DATA Data;

spec(struct vcc(claimable) _DATA_CONTAINER {
  int dummy;
  invariant(keeps(&DataLock))
  invariant(DataLock.protected_obj == &Data)
} DataContainer;
)

void testit(claimp(c))
  always(c, closed(&DataContainer))
{
  Acquire(&DataLock spec(c));
    unwrap(&Data);
      Data.a = 5;
      Data.b = 7;
    wrap(&Data);
  Release(&DataLock spec(c));
}

void boot()
  writes(set_universe())
  requires(program_entry_point())
{
  spec(claim_t c;)

  Data.a = 42;
  Data.b = 17;
  wrap(&Data);
  InitializeLock(&DataLock spec(&Data));
  set_owner(&DataLock, &DataContainer);
  wrap(&DataContainer);

  spec(c = claim(&DataContainer, closed(&DataContainer)); )
  testit(spec(c));
}

Globals of primitive types

They are implicitly surrounded by anonymous structures. Therefore if you want to own or claim it, use gemb(&global). Using emb(&global) will also mostly work, but it is slightly harder on the prover and requires that the global is considered to be typed (which is always is, but the prover might not see it).

The syntax also works for global arrays of primitive types, to own such an array say set_in(gemb(&arr), owns(this)), or alternatively set_in(gemb(&arr[0]), owns(this)), in particular the as_array(...) should not be used.

Please note that it might be necessary to specify the owns-set of the embedding struct before wrapping it set_owns(gemb(&global), set_empty()).

#include <vcc.h>

int x;

struct A {
  int y;

  spec(claim_t c;)

  invariant(keeps(c) && claims(c, closed(gemb(&x))))
  invariant(y < by_claim(c, x))
};

spec(struct vcc(claimable) _GlobalOwner {
  int dummy;
  invariant(keeps(gemb(&x)))
} GlobalOwner;
)

struct A a;

void init()
  writes(set_universe())
  requires(program_entry_point())
{
  spec(claim_t c;)

  x = 42;
  wrap(gemb(&x));

  set_owns(&GlobalOwner, set_singleton(gemb(&x)));
  wrap(&GlobalOwner);

  a.y = 12;
  spec(
    c = claim(&GlobalOwner, true);
    a.c = c;
    set_owns(&a, set_singleton(c));
    wrap(&a);
  )
}