VeriFast can’t correctly handle named fractions of char arrays that are part of a struct.

[amintimany]

VeriFast can’t correctly handle named fractions (dummy fractions don’t trigger this error) of char arrays that are part of a struct.

The following code:

struct strc {
 char chrs[3];//interestingly 1 does not trigger the error
};

void error(struct strc *x)
    //@ requires [?f]chars(x->chrs, 3, _);
          // it seems that the length (3 here) must be greater than or equal to
          // the length of the array in the struct to trigger the error.
    //@ ensures true;
{
free(x);
}

causes VeriFast to crash (exception with Redux prover and seg-fault with z3).