--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on April 2014 ---
On Tue, Apr 22, 2014 at 10:30 AM, Virgile Prevosto <virgile.prevosto at m4x.org > wrote: > 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. I had not interpreted it this way. This seems interesting but if it is to be interpreted this way (as a consistency check between requires and assigns of the same contract independently of the implementation), here is another example to consider: /*@ ... requires endptr == \null || \valid(endptr) ; assigns *endptr \from nptr[0 ..] ; ... */ double strtod(const char *restrict nptr, char **restrict endptr); where *endptr is listed in the assigns of the contract but the pre-condition does not guarantee that it is valid. There is a \valid(endptr) and one may decide it is enough for not emitting the warning, but I am not convinced. The following contract does not have a \valid requires clause that can easily be matched to the assigns clause: /*@ ... requires \valid_string(src) ; requires \valid(dst + (0 .. max(n, \string_length(src))) ; assigns dst[0 .. n-1] ; ... */ char * strncpy(char *restrict dst, const char *restrict src, size_t n); -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140422/0cc31ad5/attachment.html>