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