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

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>