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

  • Subject: [Frama-c-discuss] specification question
  • From: tim.newsham at gmail.com (Tim Newsham)
  • Date: Mon, 17 Aug 2015 18:06:46 -1000
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>