--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on April 2020 ---
Hello, Le jeu. 30 avr. 2020 à 11:21, Mike <tankf33der at disroot.org> a écrit : > hi all, > > I am having fun with testing Monocypher crypto software. > This is unique one file library passing TIS, Compcert and Frama-C (eva, > e-acsl-gcc.sh). > > > https://frama-c.com/download/e-acsl/e-acsl-manual-20.0-Calcium.pdf > page 26, example demo steps over -RTE works, but failed on library test > suite. > The same error for Frama-C versions 19 and 20: > > [kernel:annot-error] /tmp/e_acsl_default96abef.i:1426: Warning: > comparison of incompatible types: ð¹ and â¤. Ignoring code annotation > Thanks for the feedback and your interest in Frama-C. There was indeed an issue in some annotations generated by RTE, but it has been fixed in the development branch (you can try it at https://git.frama-c.com/pub/frama-c), and the fix will appear in the upcoming Frama-C 21 (Scandium). With the current master, e-acsl-gcc.sh --rte=all monocypher.c generates an instrumented file (using monocypher 3.1.0), albeit with a lot of warning stemming from the fact that E-ACSL does not support bitwise operations in ACSL annotations. Best regards, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200430/177de153/attachment.html>