thread_local vs. global pointer

Sep 28, 2009 at 4:55 PM
Edited Sep 28, 2009 at 5:17 PM

Hi there,

in our verification effort we recently got stuck with some issue when passing a global spec pointer to a function. see the following minimal example:

 

#include "vcc.h"

typedef struct O_str {
int a;
} *O_t;

spec(O_t P;)

void foo(spec(O_t O))
requires(wrapped(O))
writes(O);

void main()
writes(P)
requires(wrapped(P))
{
assert(wrapped(P));
assert(thread_local(P));
foo(spec(P));
}

 

Although we can assert thread-locality before the function call vcc complains that it cannot assert it during the call of "foo"

We are quite puzzled... but obviously it has something to do with the passing of P as a parameter

 

EDIT:

all-clear! we solved it...

when i thought about it again it became clear that we also need ownership of the global pointer itself.

adding "requires(thread_local(gemb(&P)))" sufficed to verify the example

 

#include "vcc.h"
EDit
typedef struct T_str {
    int c;
} T_t;

typedef struct S_str {
    int b;
    T_t *t;
} S_t;

typedef struct O_str {
    int a;
} *O_t;


spec(O_t P;)

void setb(S_t * s,int val)
maintains(mutable(s))
maintains(thread_local(P))
writes(&s->b)
{
    s->b = val;
}


void inc(T_t * t spec(O_t O))
//requires(thread_local(O))
writes(O)
writes(t);

void foo(spec(O_t O))
writes(O);

void main(T_t * t, int val)
//writes(&s->b)
//writes(t)
writes(P)
//requires(thread_local(P))
requires(wrapped(P))
//requires(mutable(t))
//requires(set_in0(s->t,owns(P)))
{
    //setb(s,val);
    assert(wrapped(P));
    assert(thread_local(P));
    //inc(t spec(P));
    foo(spec(P));
    //assert(false);
}
#include "vcc.h"

typedef struct O_str {
int a;
} *O_t;

spec(O_t P;)

void foo(spec(O_t O))
requires(wrapped(O))
writes(O);

void main()
writes(P)
requires(wrapped(P))
{
assert(wrapped(P));
assert(thread_local(P));
foo(spec(P));
}