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 plugin - asin function

  • Subject: [Frama-c-discuss] Eva plugin - asin function
  • From: rovedy at gmail.com (Rovedy Silva)
  • Date: Fri, 5 Jun 2020 11:00:31 -0300
  • In-reply-to: <mailman.1.1591178411.21890.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.1.1591178411.21890.frama-c-discuss@lists.gforge.inria.fr>
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>