Frama-C-discuss mailing list archives

rovedy at gmail.com (Rovedy Silva) · Thu, 21 May 2020 13:35:09 -0300

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>

Frama-C-discuss mailing list archives

[Frama-c-discuss] Frama-c-discuss Digest, Vol 143, Issue 17