Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] question about treatment of assigns clauses in WP (Neon)
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 22 Apr 2014 09:53:47 +0200
  • In-reply-to: <CA+yPOVhMvDsmkYo8VgqcZ7Zgp=h8yVBpwu2Gy90_TA7ZWhUaKw@mail.gmail.com>
  • References: <A246AA9F-4050-4278-A52E-9E9CDC45AD7B@fokus.fraunhofer.de> <CA+yPOVhMvDsmkYo8VgqcZ7Zgp=h8yVBpwu2Gy90_TA7ZWhUaKw@mail.gmail.com>
On Tue, Apr 22, 2014 at 9:37 AM, Virgile Prevosto
<virgile.prevosto at m4x.org>wrote:

> However, I think
> that in this case, there is some potential for such a warning to
> trigger a certain number of false positives in presence of
> behaviors[1]. If we take for instance the following (purely
> theoretical, I admit that I haven't seen something like that in real
> code) contract:
>
>
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, which would be
counter-productive. It is the very nature of specifications to be
abstractions of implementations. Warning that a specification is not the
tightest specification of the implementation would be backwards.

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140422/8fd224e1/attachment.html>