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: Thu, 12 Jan 2017 08:52:55 +0100
  • In-reply-to: <CALOET+AOg3mBjF0ossPug_vL_kSLJoiTi+hJuBD9-=Em8D3SVg@mail.gmail.com>
  • References: <CALOET+C5w4LkPiHOd9k3OzDcCWJQTZ6rzhh3jU=QeQ3dNUCF-g@mail.gmail.com> <CA+yPOVh-Zj8vUfLqmka1WtN2yLAgK4050eyacbv8UrGJtSgbVg@mail.gmail.com> <CALOET+AOg3mBjF0ossPug_vL_kSLJoiTi+hJuBD9-=Em8D3SVg@mail.gmail.com>
Hello,

2017-01-12 0:48 GMT+01:00 Faraz Hussain <fh.faraz.hussain at gmail.com>:

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

> Thank you very much!   Adding the implementation for fabsf inside wrong25.c
> made the warning go away.  It also removed the following warning, that was
> related to the same function:
>
> /mnt/local/csmith/runtime/safe_math.h:959:[value] warning: non-finite float
> value.
>                  assert \is_finite(tmp);
>                  (tmp from fabsf(0.5f * sf1 + 0.5f * sf2))

That's normal. As long as fabsf was neither defined nor specified, EVA
did assume that it could return infinity or nan, and complained as
soon as its result was used. Now that you have a definition, EVA can
see that the returned value is finite.

>
>
> However, I do not want to have to add the implementation to all the files
> individually.  But, adding it to math.c did not work. Is this because
> frama-c now has to be rebuilt?  How do I rebuild, considering that I had
> originally installed it using the OPAM based method ?
>

No, Frama-C does not need to be rebuilt (note however that you might
want to put your own definitions in another file in order to prevent
issues if you update Frama-C at some point).
As mentioned above, if you want to use the definitions of math.c, you
have to tell Frama-C to parse math.c in addition to wrong25.c, i.e.
your command line should be of the form

  frama-c wrong25.c $(frama-c -print-share-path)/libc/math.c [other options]

wrong25.c has #include directive for the headers, but of course not
for the corresponding implementations, hence they have to be added
explicitly whenever they are needed.

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