--- layout: fc_discuss_archives title: Message 11 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,

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

It means that these annotations are not checked at runtime.

BTW the E-ACSL support for ACSL bitwise operations is planned to be 
available in the Git repo in a few weeks :-).

Best regards,
Julien