This project is read-only.

\thread_local_array no longer implies that the pointers to each element of the array are not NULL?

Feb 16, 2013 at 10:27 PM
In order to get an implementation of strchr to verify, I am needing to add a _(requires) annotation that each pointer to an element of a thread-local array is not NULL:
_(pure) char *strchr(const char *str, int c _(ghost size_t nul_pos))
    _(requires \forall size_t i; i < nul_pos + 1 ==> str + i != 0) // <-- HERE
    _(requires \thread_local_array(str, nul_pos + 1))
    _(requires str[nul_pos] == '\0')
    _(requires -128 <= c && c <= 127) // http://vcc.codeplex.com/discussions/252475
    _(reads \universe()) // http://vcc.codeplex.com/discussions/252343#post591593
    _(ensures \result == 0 <==> (\forall size_t j; j <= strlen(str, nul_pos) ==> str[j] != (char) c))
    _(ensures \result != 0 ==> (\forall size_t j; j < ((size_t)(\result - str)) ==> str[j] != (char) c) && *\result == (char) c)
    _(ensures \result != 0 ==> (\forall size_t k; k <= strlen(str, nul_pos) && (\forall size_t j; j < k ==> str[j] != (char) c) && str[k] == (char) c ==> \result == str + k))
    ;
Shouldn't \thread_local_array imply that each pointer to an element in the array is not NULL?