--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)



Hello,

2014-04-22 8:57 GMT+02:00 BAUDIN Patrick <Patrick.Baudin at cea.fr>:
> You are looking for stronger semantics...
> It seems you want a new clause :
> - stronger_assigns *(a+(0..n));
> which can be automatically rewritten into a normal
> - assigns *(a+(0..n));
2014-04-22 9:53 GMT+02:00 Pascal Cuoq <pascal.cuoq at gmail.com>:
> A non-theoretical example is the specification of, say, standard function
> fseek():
>
> /*@ ...
>   assigns *stream \from offset, whence;
>   ....
> */
> int fseek(FILE *stream, long offset, int whence);
>
> This function does not assign the entire *stream for any of its arguments,
> so the proposed warning would be emitted,
> For initialization functions, a way to specify that a memory location must
> be written to by the function could be useful, but that way is not an assigns clause.

I might have misunderstood what Jens is saying, but to me this has
nothing to do with the notion of "strong" assigns (i.e. locations that
are guaranteed to be written by a function). In addition, assuming
that fseek has some requires \valid(stream); clause in the ... part,
I'd say that the hypothetical warning won't be triggered: the point is
just to check that all occurrences of *p in assigns are guarded by a
\valid(p) in requires. It'd just act as a consistency check for the
specification itself, without any reference to an implementation which
might not even exist in the first place.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile