Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] EVA: understanding behaviors for undefined functions
  • From: fh.faraz.hussain at gmail.com (Faraz Hussain)
  • Date: Mon, 9 Jan 2017 17:19:41 -0700
  • In-reply-to: <CALOET+C5w4LkPiHOd9k3OzDcCWJQTZ6rzhh3jU=QeQ3dNUCF-g@mail.gmail.com>
  • References: <CALOET+C5w4LkPiHOd9k3OzDcCWJQTZ6rzhh3jU=QeQ3dNUCF-g@mail.gmail.com>
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>