--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on August 2015 ---
Hi, Specifying variadic functions is tricky, because ACSL offers no support. There is unfortunately no fully satisfying solution currently, although we expect the situation to improve in Frama-C Aluminium. When the format is statically known, you can specialize each call to the variadic function, and write the corresponding specification: #include "stdio.h" //@ assigns *p, \result \from \nothing; ensures \result == 0 || (\result == 1 && \initialized(p)); int fscanf_u(FILE *stream, const char *format, unsigned int *p); //@ ensures \result == 1 ==> \initialized(retp); // Not the required, present to check that the specification of fscanf_u works. static int readUInt(FILE *fp, unsigned int *retp) { if(fscanf_u(fp, "%u", retp) == 1) return 1; return 0; } void main() { unsigned int x; readUInt (0, &x); } This program can be fully analyzed and proved with -slevel 2. I simplified a bit the specification of fscanf_u, which should contain a precondition for stream, and something depending on stream in the \from clause. HTH, On Tue, Aug 18, 2015 at 9:13 PM, Tim Newsham <tim.newsham at gmail.com> wrote: > > > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > -- Boris -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150826/676dfc63/attachment.html>