--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2020 ---
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>