--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on May 2020 ---
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>