--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on April 2014 ---
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