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: david.buhler at cea.fr (David Bühler)
  • Date: Tue, 19 May 2020 09:42:07 +0200
  • In-reply-to: <CAFd8C1WwV43d=nC_E=ex6uR8moqSM+bCFZnS2eAgTg+kHT1aqQ@mail.gmail.com>
  • References: <CAFd8C1WwV43d=nC_E=ex6uR8moqSM+bCFZnS2eAgTg+kHT1aqQ@mail.gmail.com>
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.html>