--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on January 2017 ---
Hello, 2017-01-10 1:01 GMT+01:00 Faraz Hussain <fh.faraz.hussain at gmail.com>: > [note] I am using Silicon-20161101, on Ubuntu 16.04. The command executed > is: frama-c -metrics -metrics-libc -cpp-command "gcc -C -Dvolatile= -E -I > ${CSMITH_HOME}/runtime" -machdep x86_64 wrong25.c > > [question] The "Neither code nor specification" message is given only for > fabsf, not the other 3 undefined functions (viz fabs, strcmp, and printf). > Why? Recall that these three were in the list of undefined functions. > [question] Where did it find the specification for printf, as the message in > the last note shown above says? First of all, recall that your usage of -metrics provides you with syntactic information, while EVA messages give you semantic information. In particular, if a particular call occurs in a dead branch (with respect to the entry point chosen for -val), it will not be considered by EVA, thus it will not emit any message related to it. This is probably why you don't see anything related to strcmp and fabs. On the other hand, printf is called during the abstract execution, but as it has a (very partial) ACSL specification in Frama-C's own standard library, EVA uses the specification and does not complain about lack of information on printf. > My aim here is to make this warning go away. My guess is that I need to > let Frama-C know the location/file where fabs is implemented? Understanding > why its not complaining about strcmp, fabs, and printf will really help > here. A certain number of annotations for standard library functions are available in $(frama-c -print-share-path)/libc/*.h, which are #included by Frama-C. For some functions, an implementation is 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 Frama-C's command line. Note that in your particular case, no implementation is provided for fabsf, but it shouldn't be too difficult to derive one from the existing fabs implementation. Such implementation can be provided directly in wrong25.c, or in another file, as it most suits you. Best regards, -- E tutto per oggi, a la prossima volta Virgile