--- layout: fc_discuss_archives title: Message 8 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,  I would like to use the following function in my
analysis (using the value analysis plugin):

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

It uses fscanf, which frama-c doesn't know too much about.
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?  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?

-- 
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/20150817/2c97c235/attachment.html>