--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Eva plugin - asin function



Hi David,

Thanks a lot for the implementations.

I like the Frama-C tool because the interaction with your team is always
very productive and useful.

Best regards,
Rovedy


Em qua., 3 de jun. de 2020 às 07:00, <
frama-c-discuss-request at lists.gforge.inria.fr> escreveu:

> Send Frama-c-discuss mailing list submissions to
>         frama-c-discuss at lists.gforge.inria.fr
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> or, via email, send a message with subject or body 'help' to
>         frama-c-discuss-request at lists.gforge.inria.fr
>
> You can reach the person managing the list at
>         frama-c-discuss-owner at lists.gforge.inria.fr
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Frama-c-discuss digest..."
>
>
> Today's Topics:
>
>    1. Re: Eva plugin - asin function (David Bühler)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Wed, 3 Jun 2020 09:58:56 +0200
> From: David Bühler <david.buhler at cea.fr>
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: Re: [Frama-c-discuss] Eva plugin - asin function
> Message-ID: <e697d9df-1ea8-ea0b-26ef-a509b1ac3245 at cea.fr>
> Content-Type: text/plain; charset="utf-8"; Format="flowed"
>
> Hi Rovedy,
>
> We have implemented new builtins for the trigonometric functions acos,
> asin and atan (and their single-precision version acosf/asinf/atanf).
> They are already available in the master branch of our public git
> repository : https://git.frama-c.com/pub/frama-c
>
> However, these builtins will not be included in Frama-C 21 (Scandium)
> coming this month, and will only be available in the next stable version
> of Frama-C, which should be released in about six months.
>
> So with the latest version of our trunk, the C code you gave in your
> first mail is now precisely analyzed:
>
> [eva] ====== VALUES COMPUTED ======
> [eva:final-states] Values at end of function main:
>    resultCos ∈ {0.866025403784}
>    resultSin ∈ {0.5}
>    resultSqrt ∈ {3.}
>    resultAtan2 ∈ {2.89846028423}
>    resultAsin ∈ {0.523598775598}
>
>
> Please note that these new builtins, as all builtins for mathematical
> functions, rely internally on the corresponding functions from the
> system libc of the machine performing the analysis. The results may
> slightly differ between different libc implementations.
>
> Best regards,
>   __
> David.
>
> Le 19/05/2020 à 09:42, David Bühler a écrit :
> > Hi,
> >
> > In the Eva analyzer, the precise interpretation of calls to the
> > standard library relies on builtins, which are ocaml functions that
> > precisely model the effects of such calls.
> >
> > However, Eva does not provide builtins for /all/ functions of the
> > libc. Option -eva-builtins-list prints the list of all available
> builtins.
> > Among trigonometric functions, we currently have builtins for cos, sin
> > and atan2, but not for acos or asin.
> >
> > When no builtin is available, the interpretation of a call to a
> > library function only relies on a ACSL specification, which is often
> > very imprecise. In the case of asin, the ACSL specification uses
> > (twice) the ACSL mathematical operator \abs, which is currently not
> > supported by Eva.
> > This explains the messages printed when the analysis reaches a call to
> > asin.
> >
> > Unfortunately, without a proper builtin for the asin function, you
> > cannot obtain a better result with the current version of Frama-C.
> >
> > Fortunately, builtins for these functions are relatively easy to
> > implement.
> > And as new builtins are only added to Eva when the need arises, I
> > would say that mailing us was the right move here.
> > We will try to implement builtins for the acos and asin functions in
> > the upcoming weeks.
> > I will keep you informed of our progress.
> >
> > Best regards,
> >  __
> > David.
> >
> > Le 15/05/2020 à 22:26, Rovedy Silva a écrit :
> >> Hello,
> >>
> >> Why the eva plugin show this message for the asin function?
> >> How do I get an exact result for the asin function as I did for the
> >> other mathematical functions?
> >> I am using the Frama-C 20.0 (Calcium).
> >> The source code and the analysis are attached bellow.
> >>
> >> Best Regards,
> >> Rovedy
> >>
> >> ———————————————— message - analysis excerpt———————
> >> [eva] using specification for function asin
> >> [eva] FRAMAC_SHARE/libc/math.h:172:
> >>   cannot evaluate ACSL term, unsupported ACSL construct: logic
> >> function \abs
> >> [eva] FRAMAC_SHARE/libc/math.h:176:
> >>   cannot evaluate ACSL term, unsupported ACSL construct: logic
> >> function \abs
> >>
> >> ———————————————— source code ————————
> >> #include "/Users/rovedy/.opam/4.05.0/share/frama-c/libc/math.h"
> >> int main()
> >> {
> >>   double resultCos, resultSin, resultSqrt, resultAtan2, resultAsin;
> >>    resultCos=cos(M_PI/6);
> >>    resultSin=sin(M_PI/6);
> >>    resultSqrt=sqrt(9);
> >>    resultAtan2=atan2(2.53, -10.2);
> >>    resultAsin=asin(0.5);
> >>    Frama_C_show_each_asin(resultAsin);
> >> }
> >> ———————————————— complete analysis  ————————
> >> $frama-c -eva eva1.c
> >>
> >> [kernel] Parsing eva1.c (with preprocessing)
> >> [kernel:parser:decimal-float] eva1.c:9: Warning:
> >>   Floating-point constant 10.2 is not represented exactly. Will use
> >> 0x1.4666666666666p3.
> >>   (warn-once: no further messages from category
> >> 'parser:decimal-float' will be emitted)
> >> [eva] Analyzing a complete application starting at main
> >> [eva] Computing initial state
> >> [eva] Initial state computed
> >> [eva:initial-state] Values of globals at initialization
> >> [eva] using specification for function asin
> >> [eva] FRAMAC_SHARE/libc/math.h:172:
> >>   cannot evaluate ACSL term, unsupported ACSL construct: logic
> >> function \abs
> >> [eva] FRAMAC_SHARE/libc/math.h:176:
> >>   cannot evaluate ACSL term, unsupported ACSL construct: logic
> >> function \abs
> >> [eva] eva1.c:11:
> >>   Frama_C_show_each_asin: [-1.79769313486e+308 .. 1.79769313486e+308]
> >> [eva] done for function main
> >> [eva] ====== VALUES COMPUTED ======
> >> [eva:final-states] Values at end of function main:
> >>   __fc_errno ∈ [--..--]
> >>   resultCos ∈ {0.866025403784}
> >>   resultSin ∈ {0.5}
> >>   resultSqrt ∈ {3.}
> >>   resultAtan2 ∈ {2.89846028423}
> >>   resultAsin ∈ [-inf .. inf] ∪ {NaN}
> >>   __retres ∈ {0}
> >> [eva:summary] ====== ANALYSIS SUMMARY ======
> >>
> ----------------------------------------------------------------------------
> >>   1 function analyzed (out of 1): 100% coverage.
> >>   In this function, 8 statements reached (out of 8): 100% coverage.
> >>
> ----------------------------------------------------------------------------
> >>   Some errors and warnings have been raised during the analysis:
> >>     by the Eva analyzer:      0 errors    0 warnings
> >>     by the Frama-C kernel:    0 errors    1 warning
> >>
> ----------------------------------------------------------------------------
> >>   0 alarms generated by the analysis.
> >>
> ----------------------------------------------------------------------------
> >>   Evaluation of the logical properties reached by the analysis:
> >>     Assertions        0 valid     0 unknown     0 invalid      0 total
> >>     Preconditions     6 valid     0 unknown     0 invalid      6 total
> >>   100% of the logical properties reached have been proven.
> >>
> ----------------------------------------------------------------------------
> >>
> >> _______________________________________________
> >> Frama-c-discuss mailing list
> >> Frama-c-discuss at lists.gforge.inria.fr
> >> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> >
> >
> > _______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200603/2a1c0a91/attachment-0001.html
> >
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
> ------------------------------
>
> End of Frama-c-discuss Digest, Vol 144, Issue 1
> ***********************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200605/409a9f68/attachment-0001.html>