--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] specification question



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>