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

[Frama-c-discuss] checking Monocypher



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:

$ e-acsl-gcc.sh -c *.c --rte=all
// skip
[rte] annotating function trim_scalar
[rte] annotating function unary_g
[rte] annotating function vector_test
[rte] annotating function wipe_block
[rte] annotating function x16
[rte] annotating function x32
[rte] annotating function x64
[rte] annotating function xor_block
[rte] annotating function zerocmp32
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl//e_acsl_gmp_api.h (with preprocessing)
[kernel] /usr/include/x86_64-linux-gnu/bits/thread-shared-types.h:151: Warning:
  unnamed fields are a C11 extension (use -c11 to avoid this warning)
[kernel] Parsing FRAMAC_SHARE/e-acsl//e_acsl.h (with preprocessing)
[kernel] Parsing /tmp/e_acsl_default96abef.i (no preprocessing)
[kernel:annot-error] /tmp/e_acsl_default96abef.i:1426: Warning:
  comparison of incompatible types: 𝔹 and ℤ. Ignoring code annotation
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "/tmp/e_acsl_default96abef.i" that has errors.
[kernel] Frama-C aborted: invalid user input.

My Ubuntu environment:
$ frama-c -v
20.0 (Calcium)
$ cat /etc/issue
Ubuntu 18.04.4 LTS \n \l
$ uname -a
Linux ubuntu 5.3.0-51-generic #44~18.04.2-Ubuntu SMP Thu Apr 23 14:27:18 UTC 2020 x86_64 x86_64 x86_64 GNU/Linux



Did I missed something?


(mike)