Yes you can. the right part of the from
indicates which locations might contribute to the value of \result
, but f
does not need to read from *p
to compute \result
(and it should better avoid it if p
is NULL
of course).
As a side note, the question could have also been raised for the assigns
clause of the p_not_null
behavior, as p!=\null
does
not imply \valid(p)
in C.
Nevertheless, the contract without behavior is slightly less precise than the one with behaviors, which states that when p
is NULL
a constant value is returned, and when p
is not null, only the content of *p
is used (the assigns
clause without behavior allows to return e.g. *p+(int)p
, or even (int)p
).