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

Hi Virgile,

On Thu, Jan 12, 2017 at 12:52 AM, Virgile Prevosto <virgile.prevosto at m4x.org
> wrote:

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


Ah, yes. That makes sense. Thanks.



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


Thank you, this is  a much cleaner solution indeed!  I actually used
`frama-c [my options] wrong25.c  mymath.c`, with options preceding the
files. Here, mymath.c contains my implementation of the required functions
(and includes math.h).

Regards
Faraz.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170113/f85118ba/attachment-0001.html>