This project is read-only.


Dec 16, 2010 at 3:52 PM


If I declare one function with vcc(atomic_inline), will it ensure that the update of that funtion is atomic?

Looking for your suggestions.


Dec 19, 2010 at 9:03 AM


  vcc(atomic_inline) does not ensure that a function update is atomic. It's effects are that the body of the function is inlined when the function is called inside of an atomic() {} block. This is typically used for the specification of interlocked compiler intrinsics (e.g., InterlockedCompareExchange()), cf. Section 7 of the tutorial,

  Hope that helps, Mark

Jan 20, 2011 at 1:40 PM
Edited Jan 22, 2011 at 4:06 PM

Hi Mark,

What is the malloc notations for the new version of the Vcc?

Feb 11, 2011 at 9:36 AM


  malloc() is the same in old and new VCC syntax: 

#include "vcc.h"
#include <stdlib.h>

struct S {
  int a;

void foo() {
  struct S *s = (struct S *)malloc(sizeof(struct S));
  _(assume s!=NULL) // assume enough memory
  // old syntax version: assume(s!=NULL);
  s->a = 42;

Best, Mark