--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on January 2017 ---
Hello, I am trying to understand the meaning of some common Frama-C warnings that I encounter. One of them is often like the following: *[value] computing for function fabsf <- safe_div_func_float_f_f <- func_2 <-* * func_1 <- main.* * Called from /mnt/local/csmith/runtime/safe_math.h:1000.* */mnt/local/csmith/runtime/safe_math.h:1000:[kernel] warning: Neither code nor specification for function fabsf, generating default assigns from the prototype* *[value] using specification for function fabsf* *[value] Done for function fabsf* Now, I just started going through the EVA manual, and read about the very helpful *-metrics *command. So here's an extract of the result of running it on my C file (emphasis mine): * Undefined functions (121)* * =========================* * __FC_assert (0 call); acos (0 call); acosf (0 call); acosh (0 call);* * acoshf (0 call); acoshl (0 call); acosl (0 call); asin (0 call);* * asinf (0 call); asinl (0 call); atan2 (0 call); bzero (0 call);* * ceil (0 call); ceilf (0 call); clearerr (0 call);* * clearerr_unlocked (0 call); cos (0 call); exp (0 call); expf (0 call);* * fabs (5 calls); fabsf (5 calls); fclose (0 call); fdopen (0 call);* * feof (0 call); feof_unlocked (0 call); ferror (0 call);* * ferror_unlocked (0 call); fflush (0 call); fgetc (0 call); fgetpos (0 call);* * fgets (0 call); fileno (0 call); fileno_unlocked (0 call);* * flockfile (0 call); floor (0 call); floorf (0 call); fmod (0 call);* * fopen (0 call); fprintf (0 call); fputc (0 call); fputs (0 call);* * fread (0 call); freopen (0 call); fscanf (0 call); fseek (0 call);* * fsetpos (0 call); ftell (0 call); ftrylockfile (0 call);* * funlockfile (0 call); fwrite (0 call); getc (0 call);* * getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);* * gets (0 call); log (0 call); log10 (0 call); log10f (0 call); logf (0 call);* * memchr (0 call); memcmp (0 call); memcpy (0 call); memmove (0 call);* * memset (0 call); nan (0 call); nanf (0 call); nanl (0 call);* * perror (0 call); pow (0 call); powf (0 call); printf (26 calls);* * putc (0 call); putc_unlocked (0 call); putchar (0 call);* * putchar_unlocked (0 call); puts (0 call); remove (0 call); rename (0 call);* * rewind (0 call); round (0 call); roundf (0 call); scanf (0 call);* * setbuf (0 call); setvbuf (0 call); sin (0 call); snprintf (0 call);* * sprintf (0 call); sqrt (0 call); sqrtf (0 call); strcat (0 call);* * strchr (0 call); strcmp (1 call); strcoll (0 call); strcpy (0 call);* * strcspn (0 call); strdup (0 call); strerror (0 call); strlen (0 call);* * strncat (0 call); strncmp (0 call); strncpy (0 call); strndup (0 call);* * strnlen (0 call); strpbrk (0 call); strrchr (0 call); strsep (0 call);* * strspn (0 call); strstr (0 call); strtok (0 call); strxfrm (0 call);* * tmpfile (0 call); tmpnam (0 call); trunc (0 call); truncf (0 call);* * ungetc (0 call); vfprintf (0 call); vfscanf (0 call); vprintf (0 call);* * vscanf (0 call); vsnprintf (0 call); vsprintf (0 call); * According to this analysis, calls are made to 4 undefined functions, viz *fabs, fabsf, printf, *and* strcmp*. Here are my questions (with some notes): [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* [note] *strcmp *and *fabs * never appear in the Frama-C output for this file (whereas *printf and fabsf *do appear*)*. [note] Here's the warning regarding *fabsf * again: *[value] computing for function fabsf <- safe_div_func_float_f_f <- func_2 <-* * func_1 <- main.* * Called from /mnt/local/csmith/runtime/safe_math.h:1000.* */mnt/local/csmith/runtime/safe_math.h:1000:[kernel] warning: Neither code nor specification for function fabsf, generating default assigns from the prototype* *[value] using specification for function fabsf* *[value] Done for function fabsf* [note] The following message is shown for *printf*: *[value] computing for function printf <- platform_main_end <- main.* * Called from /mnt/local/csmith/runtime/platform_generic.h:56.* *[value] using specification for function printf* [note] The relevant files are attached. [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? 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. The EVA manual (pg. 17) says that "Not having a body for printf is fine, since calls to this function have no observable effects for the analysis." I think the same may be true of this program. If so, that leaves us with *strcmp, *and *fabs -- * the metrics command lists both of these are undefined, so why doesn't the EVA complain about these two the way it complained about *fabsf *? Many thanks for reading this long email! Regards Faraz. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170109/bd385ae8/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: wrong25.c Type: text/x-csrc Size: 188332 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170109/bd385ae8/attachment-0001.c> -------------- next part -------------- A non-text attachment was scrubbed... Name: safe_math.h Type: text/x-chdr Size: 24944 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170109/bd385ae8/attachment-0001.h>