--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on August 2015 ---
On Mon, Aug 17, 2015 at 10:12 PM, David MENTRE <dmentre at linux-france.org> wrote: > It uses fscanf, which frama-c doesn't know too much about. >> > > Just #include <stdio.h>, with Frama-C Sodium you'll have properly > annotated headers by default. > > frama-c-gui -val -main readUInt tim-fprintf.c Sure, it is in stdio.h, but it does not know anything about the var-args assigning behavior of fscanf: <from stdio.h> /*@ assigns *stream; // unsupported... */ int fscanf(FILE * restrict stream, const char * restrict format, ...); <end stdio.h> What sort of annotations would be appropriate >> to let it know that when readUInt returns 1 the value of *retp will >> be assigned to with an unspecified value? >> > > Probably something like (not tested): > > ensures \result == 1 ==> \initialized(retp); > I tried using an annotation like this (see attached) and when using "frama-c-gui -val -main readUInt tim-fprintf.c" it marked the ensures annotation as yellow. > In Frama-C header __fc_builtin.h you also have "Frama_C_entropy_source" > that you can use as source of randomness. See __fc_builtin.h for examples > of use. > For my own project, I ended up using an #ifdef for this one function to provide a model that uses entropy, instead of using the real fscanf implementation. I guess it works best in this case.. Thank you for the feedback! Best regards, > david > -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150818/2d284384/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: tim-fprintf.c Type: text/x-csrc Size: 208 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150818/2d284384/attachment-0001.c>