--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on September 2013 ---
[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?



On Fri, Sep 6, 2013 at 7:51 AM, Steven Stewart-Gallus <
sstewartgallus00 at mylangara.bc.ca> wrote:

> /*@
>   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);
>
> How would one attach an annotation to a function declared in an external
> header?
>
>
In any file that you like (it can be a .c file and it will not be necessary
to include it more than once in any analysis project), you can repeat the
prototype of the function and attach a contract to it.

In practice, you could have a fread_spec.c file containing:

#include <stdlib.h>
#include <stdio.h>
/*@
  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);

? and list this file on the command-line as often as necessary:

frama-c ? myapp1.c myapp2.c fread_spec.c

You would be better off using the headers provided with Frama-C in
share/libc than your system's header. They already have specifications for
some functions. This can be achieved by pre-processing with "gcc -nostdinc
-I?"

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130906/4129ccbb/attachment.html>