This project is read-only.

Invariant lost when \wrapped() in implies

Feb 8, 2013 at 4:37 AM
Hi,

I got a strange problem. The invariant information is lost, when I wrap an object in some condition. Does anyone have some idea about this?

Thanks very much in advance.
typedef struct {
    unsigned prio;
    _(invariant prio < 7)
} st;

st * Temp;

void foo(void *tPara)
    _(requires tPara != NULL ==> \wrapped((st *) tPara))
    //_(requires tPara != NULL ==> ((st *)tPara)->prio < 7)
    _(requires \thread_local(&Temp))
    _(updates Temp)
{
    st * test;
    _(assume tPara != NULL)
    test = tPara == NULL ? Temp : (st *) tPara;
        _(assert test == ((st *) tPara))
            _(assert test->prio < 7) //********FAIL*******
}

void foo1(void *tPara)
    _(requires tPara != NULL ==> \wrapped((st *) tPara))
    //_(requires tPara != NULL ==> ((st *)tPara)->prio < 7)
    _(requires \thread_local(&Temp))
    _(updates Temp)
{
    st * test;
    _(assume tPara == NULL)
    test = tPara == NULL ? Temp : (st *) tPara;
        _(assert test == ((st *) tPara))
            _(assert test->prio < 7)
}
For function void foo(void ) and void foo1(void ), I need to access the ((st ) tPara)->prio and Temp->prio respectively, which depends on whether tPara is NULL. However, I actually lost the constraint information for struct st tPara. VCC complain that in fuction void foo(void *), test->prio < 7 did not verify.
Feb 11, 2013 at 9:20 PM
Hi there,

invariant constraint are not automatically visible in functions, for performance reasons. In foo(), there is nothing that "triggers" VCC to take advantage of the structure invariants. To fix, you can add "_(assert \inv(((st *) tPara)))" or "_(assert ((st *) tPara \in \domain((st *) tPara)))" before you failing assertion. Please note, that in certain cases, VCC add assertions such as these automatically to the certain places in the function (e.g., the beginning) ("inference"). For example, for "_(requires \wrapped(x))" would have implicitly added "_(assert (x) \in \domain(x))" by default. However, because in your case, the requirement is conditional ( ... => \wrapped(x)), this doesn't trigger. More information is in VCC's documentation.

Hope this helps,

Mark