This project is read-only.

the question :VCC how to deal with global variable

Jun 11, 2015 at 10:33 AM
Hi everyone,

I have some questions about how to deal with the global structure variables, hope can someone can help me.

for example,this is the program(initset.c).

typedef struct task{
            int a;
            int b;
}task;

task *tk;
int c;
void set(int a,int b,int m )
{
           tk->a=a;
           tk->b=b;
            c=m;
}

In order to verify this,I write the VCC annotation like this:
(1)
typedef struct task{
            int a;
            int b;
           _( invariant a<b)
}task;

task *tk;
int c;

void set(int a,int b ,int m)
_(requires a<b)
_(requires \thread_local(tk))
_(requires \wrapped(tk))
_(writes tk)
_( writes &c)
{
           _( unwrap tk)
           _( assert \mutable (tk))
           _( assert \thread_local (tk))
           tk->a=a;
           tk->b=b;
            c=m;
           _( wrap tk)
}

but There is a error:"Assertion 'tk is thread local (accessing field data)' did not verify."

So I modified the annotation as follows:
(2)
typedef struct task{
            int a;
            int b;
           _( invariant a<=b)
}task;

task *tk;
int c;
typedef struct task2{

}task2;

task2 tk2;

void init(task2 *t2)
_(requires \program_entry_point() )
_(requires t2-> \owns=={} )
_(requires \mutable(t2))
_(writes \span(t2))
{
_(ghost t2-> \owns+=tk;)
_(wrap t2)
}

void set(int a,int b )
_(requires tk \in (&tk2)->\owns )
_(requires \wrapped(&tk2))
_(requires a<b)
_(writes &tk2)
_( writes &c)
{
           _( unwrap (&tk2))
                          _( ghost (&tk2)->\owns -=tk;)
           _( unwrap tk)
           _( assert \mutable (tk))
            //_(assert \wrapped(tk))
           tk->a=a;
           tk->b=b;
           c=m;
           _( wrap tk)
           _( ghost (&tk2)->\owns +=tk;)
           _( wrap &tk2)
}

happily, vcc said " verification succeeded"。But , I found it is always " verification succeeded" no matter what I have write , for example the statement "_(assert \wrapped(tk)) "。I known if I write the statements that confict with each other,vcc will always report " verification succeeded " ,nut there is no confict.


So, I hope someone can hope me figure out follows questions.
(1) why does my first approach is wrong? even I have do the hypothsis.
(2) experienced staff will how to deal with the glocal variable("task *tk" and " int c") ,especially the glocal structure(pointer) variable?
(3)what circumstances will make VCC always report " verification succeeded" ?

I really need the answer . if could ,I hope someone can illustrate how to verifiy the "initset.c".

looking forward to the reply!