--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on January 2017 ---
Hello, 2017-01-12 0:48 GMT+01:00 Faraz Hussain <fh.faraz.hussain at gmail.com>: >> available in a corresponding *.c file in the same directory. In order >> to use such a definition (as opposed to a specification), you have to >> add the .c file to the list of source files that have to be parsed on > Thank you very much! Adding the implementation for fabsf inside wrong25.c > made the warning go away. It also removed the following warning, that was > related to the same function: > > /mnt/local/csmith/runtime/safe_math.h:959:[value] warning: non-finite float > value. > assert \is_finite(tmp); > (tmp from fabsf(0.5f * sf1 + 0.5f * sf2)) That's normal. As long as fabsf was neither defined nor specified, EVA did assume that it could return infinity or nan, and complained as soon as its result was used. Now that you have a definition, EVA can see that the returned value is finite. > > > However, I do not want to have to add the implementation to all the files > individually. But, adding it to math.c did not work. Is this because > frama-c now has to be rebuilt? How do I rebuild, considering that I had > originally installed it using the OPAM based method ? > No, Frama-C does not need to be rebuilt (note however that you might want to put your own definitions in another file in order to prevent issues if you update Frama-C at some point). As mentioned above, if you want to use the definitions of math.c, you have to tell Frama-C to parse math.c in addition to wrong25.c, i.e. your command line should be of the form frama-c wrong25.c $(frama-c -print-share-path)/libc/math.c [other options] wrong25.c has #include directive for the headers, but of course not for the corresponding implementations, hence they have to be added explicitly whenever they are needed. Best regards, -- E tutto per oggi, a la prossima volta Virgile