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] How would one annotate a function in an external header?

Hello Steven,

Disclaimer: I'm also learning Frama-C. ;-)

2013/9/6 Steven Stewart-Gallus <sstewartgallus00 at mylangara.bc.ca>:
> I'm interested in exploring Frama-C in an unusual manner which is by creating a
> tiny toy 3D game application. I plan on making this feasible by dividing my
> application up into several isolated processes that communicate through message
> passing.

You are probably aware of it but a Frama-C plug-in to check concurrent
applications has been recently released by Adelard:
  https://bitbucket.org/adelard/simple-concurrency/

> All my unverified code which will struggle against large, ugly, and
> unsafe APIs like OpenGL, or SDL will be contained inside separate processes
> (sort of like Google's Chromium.) There is currently, an ongoing attempt to
> formalise, and provide annotations for the standard libraries APIs but
> unfortunately not that much has been done yet. For that reason, I wish to write
> some of my own annotations such as the following (probable incorrect [I'm still
> pretty new at using frama-c]) one for the fread function which is is supposed to
> declare that the fread function initializes the data it reads into.
>
> /*@
>   ensures ? integer ii;
>   ii >= 0 ? ii < \result * size ? \initialized(&((char *)ptr)[ii]);
> */
> extern size_t fread(void *ptr, size_t size, size_t nmemb, FILE *stream);

You can test that your annotation is syntactically correct by simply
launching Frama-C on it. Please notice that depending on plug-in you
want to use later, the set of understood annotations varies greatly.
You need to check the corresponding plug-in manual.

Regarding the correctness of your annotation, I don't know. But you
might find simpler way to write it: it is better to avoid quantifiers
if possible, it complicates verification.

I would try an untested "ensures \initialized(&((char *)ptr)+(0..
((\result - 1) * size)));"

In Frama-C libc headers, notation "((char*)ptr)[0..(nmemb*size)]" is used:

/*@ assigns ((char*)ptr)[0..(nmemb*size)] \from *stream; */
size_t fread(void * restrict ptr,
     size_t size, size_t nmemb,
     FILE * restrict stream);


> How would one attach an annotation to a function declared in an external header?

Well, in the external header itself. If you include "external.h", put
your annotations in this file. In any case, you probably want to copy
them in a separate location (e.g. from /usr/lib to $HOME) to modify
them. You will probably need to replace inclusion of standard headers
by Frama-C ones which are properly annotated for Frama-C. I would look
at them in FRAMA_C_PATH/share/frama-c/libc/, it will probably give you
some ideas to properly annotate your headers. This assume you will use
WP or Jessie for verification. If you use value, you probably want to
include in your project *.c files from
FRAMA_C_PATH/share/frama-c/libc/.

Or maybe I misunderstood your question?

In any case, I find your approach of annotating standard headers very
interesting. If you can prove some properties in your program (e.g no
RTE), it could be worthwhile to propagate those headers upstream (or
at least try to ;-) ).

Best regards,
david