--- layout: fc_discuss_archives title: Message 34 from Frama-C-discuss on May 2020 ---
Hi David, Thanks a lot! So, we will wait for the implementations. We used the Frama-C Neon-20140301 to verify a part of an embedded aerospace control software in 2014. The employed mathematical functions were cos, sqrt, sin, and fabs. Now, we would like to verify a new navigation algorithm that it use the following mathematical functions: cos, sqrt, sin, atan2, and asin. So, your implementations it will be very useful for us and, I hope, for another people too!!! Best regards, Rovedy Em ter., 19 de mai. 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: [PROVENANCE INTERNET] Re: Frama-c support for dynamic > memory (Julien Signoles) > 2. Re: Eva plugin - asin function (David Bühler) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 19 May 2020 08:36:32 +0200 > From: Julien Signoles <julien.signoles at cea.fr> > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] [PROVENANCE INTERNET] Re: Frama-c > support for dynamic memory > Message-ID: <0743f196-77d9-60e5-ece9-1b07cd122468 at cea.fr> > Content-Type: text/plain; charset=utf-8; format=flowed > > Le 18/05/2020 à 09:11, WILLIAMS Nicky a écrit : > > PathCrawler, the structural test generation plugin of Frama-C, treats > dynamic allocation too. > > As well as E-ACSL, the runtime verification plug-in of Frama-C. > Dynamic allocations are much easier to handle with dynamic analysis > tools :-). > > Julien > > > ________________________________________ > > From: Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] > on behalf of Claude Marche [Claude.Marche at inria.fr] > > Sent: 18 May 2020 09:09 > > To: frama-c-discuss at lists.gforge.inria.fr > > Subject: Re: [Frama-c-discuss] Frama-c support for dynamic memory > > > > Hello Mike, hello to all, > > > > Le 18/05/2020 à 03:21, Whalen, Mike a écrit : > >> Hello all, > >> > >> Apologies for perhaps an unfair criticism of the WP manual. It is > >> really a nice document, and I have been able to prove some interesting > >> things. However, if we wish to use frama-c for AWS-related projects, we > >> must have support for dynamic memory. > > Interesting to learn that AWS aims at formally verifying C code. It is > > of course legitimate that you investigate on the existing tools to do so. > > > > Your analysis about capabilities of Frama-C and the WP plugin seems > > accurate to me. Let me add a few points that may make your analysis even > > more informed > > > > * verifying C code involving complex data-structures, including dynamic > > memory allocation, remains nowadays a complex task and a complex problem > > that is the subject of many on-going research in academia. It is not the > > case that you could find a perfect tool that would suit your needs > > off-the-shelf > > > > * Using techniques based on deductive verification is certainly > > promising, however for industrial needs I think it is important to have > > a broader vision and be ready to use several different techniques. For > > example regarding using Frama-C I was wondering if you investigated the > > Eva plug-in and how Eva and WP can be used in combination? > > > > * a less academic point : developing verification environment like > > Frama-C and make them reasonably usable from an industrial perspective > > costs a lot of human resources and money. Frama-C and WP are freely > > available, their development were and are supported in part by French > > public funding and in part by collaborations and contracts with > > industrial users. Is AWS considering a collaboration with the Frama-C > > developer team, with corresponding funding? [Disclaimer: I'm not member > > of Frama-C devteam, not a member of the CEA institute... yet I am paying > > taxes in France...] > > > >> In looking at more of the plug-ins, it appears that Jessie is built on > >> top of separation logic. It is still referenced in the frama-c web > >> site, but is it still supported? The documentation was a bit sketchy. > > Being the main and almost only remaining maintainer of Jessie, I can say > > that they are current developments for porting it to recent Frama-C > > versions, but the development is now stopped due to absence of funding. > > > > Have a nice day, take care, > > > > - Claude > > _______________________________________________ > > 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 > > > > ------------------------------ > > Message: 2 > Date: Tue, 19 May 2020 09:42:07 +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: <8f7e1775-953f-4aa1-9c74-0932cc418ac7 at cea.fr> > Content-Type: text/plain; charset="utf-8"; Format="flowed" > > 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 > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200519/baa2cacb/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 143, Issue 17 > ************************************************ > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200521/82712255/attachment-0001.html>