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:01:50 -0700
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>