--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on August 2015 ---
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>