_(writes) clause error VC8510

Apr 24, 2013 at 9:23 AM
Edited Apr 24, 2013 at 9:38 AM
Hi all,

I got this error in simple function, I am not sure what I am doing wrong. Does anybody know what I am missing?

error VC8510: Assertion '\extent(N) is writable in call to init(N)' did not verify.

This error occurs even if I use \span(N) in write clause or just type _(writes N->x).
#include <vcc.h> 
#include <stdlib.h>

typedef struct A { 
 
    struct A *x; 
    struct A *y; 
 
} A;

void init(A *N) 

_(writes \extent(N)) 

{
    N->x = NULL;    
} 

int main() 
{ 
    A *N = NULL;

    init(N);
}
Thanks Jan.
Apr 25, 2013 at 5:20 PM
This is because your pointer N in main() isn't writable. It's a NULL pointer. Following main() may help
int main() {
    A * N = (A *) malloc(sizeof(A));
    _(assume N) // malloc() may fail
    init (N);
}
Apr 26, 2013 at 8:41 AM
Ok thanks Shu,

it helps, but I have the same problem with next function after init(), again _(writable) clause, it seems I need to somehow set N for main function and keep it, but how?
typedef struct A {  
    struct A *x;  
} A;

void init(A *N) 

_(writes \extent(N)) 
_(ensures \wrapped(N))
{
    N->x = NULL; 
    _(wrap N)
} 

void actualize(A *N) 

_(writes \span(N))
_(maintains \wrapped(N))
{
    _(unwrapping N){
        N->x = NULL;    
    }
} 

void dispose(A *N) 

_(writes \span(N))
_(requires \wrapped(N))
{
    _(unwrap N)
    free(_(A*)N);
} 

int main() 
{ 
    A *N = (A*) malloc(sizeof(A));
    _(assume N)

    init(N);

    actualize(N);

    dispose(N);
}
VCC:
error VC8510: Assertion '\span(N) is writable in call to actualize(N)' did not verify.
error VC8510: Assertion '\span(N) is writable in call to dispose(N)' did not verify.

Thanks for any suggestion.
Jan
Coordinator
Apr 26, 2013 at 5:48 PM
Hi,

_(writes \span(N)) and _(requires \wrapped(N)) are contradictory - you can't have an object wrapped and at the same time have its fields writable. It should work when you use _(writes N) in actualize() and dispose().

Hope that helps, Mark
Apr 26, 2013 at 7:11 PM
Mark, if I understant you right you suppose something like this:
typedef struct A {  
    struct A *x;  
} A;

void init(A *N) 

_(writes \extent(N)) 
{
    N->x = NULL; 
} 

void actualize(A *N) 

_(writes N)
{
    N->x = NULL;  
} 

void dispose(A *N) 

_(writes N)
{
    free(_(A*)N);
} 

int main() 
{ 
    A *N = (A*) malloc(sizeof(A));
    _(assume N)

    init(N);
    _(assume N->x == NULL)

    actualize(N);

    dispose(N);
}
BUT its still the same case --> problem with _(write) clause:

Verification of init succeeded. [0,62]
Verification of actualize failed. [0,11]
error VC8507: Assertion 'N->x is writable' did not verify.
Verification of dispose failed. [0,79]
error VC8510: Assertion '\extent(p) is writable in call to free(_(A*)N)' did not verify.
error VC9502: Call 'free(_(A*)N)' did not verify.
error VC9599: (related information) Precondition: 'the extent of the object being reclaimed is mutable'.
error VC9599: (related information) Precondition: 'the pointer being reclaimed was returned by malloc()'.
Verification of main failed. [0,12]
error VC8510: Assertion 'N is writable in call to actualize(N)' did not verify.
error VC8510: Assertion 'N is writable in call to dispose(N)' did not verify.

Thanks
Jan
Coordinator
Apr 27, 2013 at 5:10 AM
Hi,

no, I was only suggesting to change the _(writes ...) clause in actualize() and dispose(), the other annotations looked fine to me.

Cheers, Mark
May 2, 2013 at 5:45 PM
MarkHillebrand wrote:
Hi,

no, I was only suggesting to change the _(writes ...) clause in actualize() and dispose(), the other annotations looked fine to me.

Cheers, Mark
Hi Mark,

I tried to verify this code. I got a error issued about free(_(A *) N) of function dispose(A *N). VCC tried to prove N is returned by malloc(). What should I do to handle this?

Best, Shu Cheng
Coordinator
May 2, 2013 at 6:09 PM
Hi,

non-NULL pointers return by malloc() satisfy the \malloc_root() predicate, which is requires in calls to free(). You need to keep track of this information, until free() is called in the dispose() function (e.g., by adding it as an invariant of struct A and as a requirement to dispose()).

Hope that helps, Mark
May 2, 2013 at 7:03 PM
Hi Mark,

Thanks very much!

I added an requirement, _(requires \malloc_root(N)), for dispose(). And it works!

Best,

Shu Cheng