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] specification question
- Subject: [Frama-c-discuss] specification question
- From: tim.newsham at gmail.com (Tim Newsham)
- Date: Tue, 18 Aug 2015 09:13:44 -1000
- In-reply-to: <55D2E8D1.10902@linux-france.org>
- References: <CAGSRWbgPO0BCmhrUR1=K-LEfQ=g-FyKQknDMTv_N0cSzeD_U7w@mail.gmail.com> <55D2E8D1.10902@linux-france.org>
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>
- Follow-Ups:
- [Frama-c-discuss] specification question
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] specification question
- References:
- [Frama-c-discuss] specification question
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] specification question
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] specification question
- Prev by Date: [Frama-c-discuss] trouble debugging assertions
- Next by Date: [Frama-c-discuss] arbitrary buffers in analysis
- Previous by thread: [Frama-c-discuss] specification question
- Next by thread: [Frama-c-discuss] specification question
- Index(es):