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

[Frama-c-discuss] specification question



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>