CODEWITHSUNDEEP
frama-c
Anne
Anne

Reputation: 1270

Use possibly invalid pointer in ACSL dependencies

I need to write an ACSL specification for the dependencies of a function that takes a pointer as input, and uses its content when the pointer in not NULL. I think that this specification is correct:

/*@ behavior p_null:
      assumes p == \null;
      assigns \result from \nothing;
    behavior p_not_null:
      assumes p != \null;
      assigns \result from *p;
*/
int f (int * p);

but I would rather avoid the behaviors, but I don't know if this is correct (and equivalent) :

//@ assigns \result from p, *p;
int f (int * p);

Can I use *p in the right part of the \from even if p might be NULL ?

Upvotes: 1

Views: 126

Answers (1)

Virgile
Virgile

Reputation: 10148

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).

Upvotes: 2

Related Questions