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

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>