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