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] 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>