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 and all,

On Tue, Jan 10, 2017 at 12:54 AM, Virgile Prevosto <virgile.prevosto at m4x.org
> wrote:

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


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


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 ?


Thanks,
Faraz.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170111/0427d68f/attachment.html>