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: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Tue, 10 Jan 2017 08:54:31 +0100
  • In-reply-to: <CALOET+C5w4LkPiHOd9k3OzDcCWJQTZ6rzhh3jU=QeQ3dNUCF-g@mail.gmail.com>
  • References: <CALOET+C5w4LkPiHOd9k3OzDcCWJQTZ6rzhh3jU=QeQ3dNUCF-g@mail.gmail.com>
Hello,

2017-01-10 1:01 GMT+01:00 Faraz Hussain <fh.faraz.hussain at gmail.com>:

> [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
>
> [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?

First of all, recall that your usage of -metrics provides you with
syntactic information, while EVA messages give you semantic
information. In particular, if a particular call occurs in a dead
branch (with respect to the entry point chosen for -val), it will not
be considered by EVA, thus it will not emit any message related to it.
This is probably why you don't see anything related to strcmp and
fabs. On the other hand, printf is called during the abstract
execution, but as it
has a (very partial) ACSL specification in Frama-C's own standard
library, EVA uses the specification and does not complain about lack
of information on printf.

> 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.

A certain number of annotations for standard library functions are
available in $(frama-c -print-share-path)/libc/*.h, which are
#included by Frama-C. For some functions, an implementation is
available in a corresponding *.c file in the same directory. In order
to use such a definition (as opposed to a specification), you have to
add the .c file to the list of source files that have to be parsed on
Frama-C's command line. Note that in your particular case, no
implementation is provided for fabsf, but it shouldn't be too
difficult to derive one from the existing fabs implementation. Such
implementation can be provided directly in wrong25.c, or in another
file, as it most suits you.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile