--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on April 2020 ---
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)