--- layout: fc_discuss_archives title: Message 30 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)



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>