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

  • Subject: [Frama-c-discuss] checking Monocypher
  • From: tankf33der at disroot.org (Mike)
  • Date: Thu, 30 Apr 2020 09:20:50 +0000
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)