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: rovedy at gmail.com (Rovedy Silva)
  • Date: Fri, 15 May 2020 17:26:28 -0300
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>