--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on January 2017 ---
I forgot to attach the result of FramaC analysis on wrong25.c -- here's a link to it (file fc.wrong25.txt, 8.2M): https://www.dropbox.com/sh/d0x2j31s8g4tpxd/AABD5kwRqq8ahZDzn5loXu0Sa?dl=0 Best Faraz. On Mon, Jan 9, 2017 at 5:01 PM, Faraz Hussain <fh.faraz.hussain at gmail.com> wrote: > 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/32a7205c/attachment.html>