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

[Frama-c-discuss] specification question



Hello,

Le 18/08/2015 06:06, Tim Newsham a écrit :
> 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


> It definitely doesn't know that *retp will be assigned if fscanf
> returns 1.  Can I inform it of that fact by adding annotations to
> my function?

Always.

>  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);

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.

Best regards,
david

-------------- next part --------------
#include <stdio.h>

static int
readUInt(FILE *fp, unsigned int *retp)
{
    if(fscanf(fp, "%u", retp) == 1)
        return 1;
    return 0;
}