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

[Frama-c-discuss] checking Monocypher



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>