--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on January 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] EVA: understanding behaviors for undefined functions



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>