--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Eva plugin - asin function



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.

----------------------------------------------------------------------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200515/c6c330b0/attachment.html>