Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002412Frama-CPlug-in > E-ACSLpublic2018-12-03 18:312018-12-17 14:03
Reporterrmalak 
Assigned Tosignoles 
PrioritynormalSeveritycrashReproducibilityalways
StatusconfirmedResolutionopen 
Platformx86_64OSLinux x86_64OS VersionDebian Sid
Product VersionFrama-C 18-Argon 
Target VersionFixed in Version 
Summary0002412: E-ACSL crash with RTE generated assertion with booleans
DescriptionThere might be a regression with the RTE or E-ACSL plugin with Argon. /////////// boolean.c #include bool return_false(void) { return false; } int main(void) { return 0; } ///////////////////////////
Steps To ReproduceOn Argon 18.0 (2f7a0eee0) : $ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c [kernel] Parsing boolean.c (with preprocessing) [rte] annotating function main [rte] annotating function return_false $ frama-c -machdep x86_64 rte_boolean.c -e-acsl [kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing) [kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing) [kernel] Parsing rte_boolean.c (with preprocessing) [e-acsl] beginning translation. [kernel] Current source was: rte_boolean.c:10 The full backtrace is: Raised at file "src/libraries/project/project.ml", line 402, characters 50-57 Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023 Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34 Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22 Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56 Called from file "queue.ml", line 105, characters 6-15 Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8 Unexpected error (Stack overflow). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is 18.0 (Argon). Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
Additional InformationOn Chlorine-20180502 (bfd93b819) : $ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c [kernel] Parsing boolean.c (with preprocessing) [rte] annotating function main [rte] annotating function return_false $ frama-c -machdep x86_64 rte_boolean.c -e-acsl [kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing) [kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing) [kernel] Parsing rte_boolean.c (with preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl".
TagsNo tags attached.
Attached Filesc file icon boolean.c [^] (118 bytes) 2018-12-03 18:31 [Show Content]

- Relationships
related to 0002419confirmedsignoles Missing cast in code generated by RTE 

-  Notes
(0006687)
signoles (manager)
2018-12-03 19:01

Thank you for the report. In 18-Argon, the RTE plug-in generates additional annotations in order to check that no trap representations are read from _Bool lvalues. These properties were not generated before 18-Argon, but are unfortunately not yet well supported by E-ACSL (as you experimented). Using -no-warn-invalid-bool would result in the 17-Chlorine's behaviour. $ frama-c -no-warn-invalid-bool -machdep x86_64 boolean.c -rte -then -e-acsl -then-last -print
(0006688)
rmalak (reporter)
2018-12-03 19:49

Hi, Thanks for the quick answer ! R.
(0006707)
rmalak (reporter)
2018-12-13 17:39

Hi ! Is this the same situation (aka RTE generates annotations that E-ACSL can't understand for now ?) or is it a totally different problem ? //////////////// unsigned-downcast.c int main(void) { int i = 1; unsigned int u_i = (i < 2); return 0; } ///////////////////////////////////// $ frama-c -machdep gcc_x86_64 -no-frama-c-stdlib unsigned-downcast.c -rte -warn-unsigned-downcast -then -e-acsl -then-last -print -ocode unsigned-downcast.e-acsl.c [kernel] Parsing unsigned-downcast.c (with preprocessing) [rte] annotating function main [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_default5edf7c.i (no preprocessing) [kernel:annot-error] /tmp/e_acsl_default5edf7c.i:6: 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_default5edf7c.i" that has errors. [kernel] Frama-C aborted: invalid user input.
(0006708)
signoles (manager)
2018-12-13 18:19

Nothing related. Here, you should use the option -e-acsl-prepare before the first -then.
(0006710)
rmalak (reporter)
2018-12-13 21:11

Thanks, $ frama-c -no-frama-c-stdlib -machdep gcc_x86_64 -e-acsl-prepare -rte -warn-unsigned-downcast unsigned-downcast.c -then -e-acsl -then-last -print -ocode unsigned-downcast.eacsl.c worked. I didn't catch at first that -e-acsl-prepare was necessary here as I thought it was for this use-case : RTE -> VAL -> E-ACSL (e-acsl-manual.pdf p24-25) and the helper script do not include the -e-acsl-prepare flag when using --rte=all (there might be something missing in the manual at p24) : $ e-acsl-gcc.sh unsigned-downcast.c -c -Ounsigned-downcast -o unsigned-downcast.e-acsl.c --rte=all + frama-c -variadic-no-translation -machdep gcc_x86_64 -cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 -no-frama-c-stdlib unsigned-downcast.c -rte -warn-signed-overflow -warn-unsigned-overflow -warn-signed-downcast -warn-unsigned-downcast -rte-div -rte-float-to-int -rte-mem -rte-pointer-call -rte-shift -rte-no-trivial-annotations -then -e-acsl -e-acsl-share=/home/jean/local-frama-c/bin/../share/frama-c/e-acsl/ -then-last -print -ocode unsigned-downcast.e-acsl.c [kernel] Parsing unsigned-downcast.c (with preprocessing) [rte] annotating function main [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_defaultaf790d.i (no preprocessing) [kernel:annot-error] /tmp/e_acsl_defaultaf790d.i:6: 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_defaultaf790d.i" that has errors. [kernel] Frama-C aborted: invalid user input.
(0006711)
signoles (manager)
2018-12-14 09:30

Actually, I though that -e-acsl-prepare was never necessary when using RTE (even if theoretically required) because I never encountered any issue... Until your post. Now, I have one example where it is required in practice :-). I will update the manual and e-acsl-gcc.sh accordingly.
(0006712)
rmalak (reporter)
2018-12-14 11:10

Cool ! Also there is something I don't understand with this damned unsigned-downcast.c example, it's the first time I am not able to do the analysis in 2 steps : RTE (with -e-acsl-prepare) and E-ACSL together $ frama-c unsigned-downcast.c -e-acsl-prepare -rte -warn-unsigned-downcast -then -e-acsl -then-last -print -ocode unsigned-downcast.e-acsl.c [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing) [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [kernel] Parsing unsigned-downcast.c (with preprocessing) [rte] annotating function main [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". RTE (with -e-acsl-prepare) $ frama-c unsigned-downcast.c -e-acsl-prepare -rte -warn-unsigned-downcast -print -ocode unsigned-downcast.rte.c [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing) [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [kernel] Parsing unsigned-downcast.c (with preprocessing) [rte] annotating function main E-ACSL on the generated intermediate unsigned-downcast.rte.c $ frama-c unsigned-downcast.rte.c -e-acsl -then-last -print -ocode unsigned-downcast.e-acsl.c [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing) [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [kernel] Parsing unsigned-downcast.rte.c (with preprocessing) [kernel:annot-error] unsigned-downcast.rte.c:25: 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 "unsigned-downcast.rte.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input. Is this a wrong usage of -then/-then-last/-e-acsl-prepare flags in the frama-c cmdline or is it a limitation of -e-acsl-prepare (I used this two steps as two targets in my Makefile without prbml until now) ?
(0006715)
signoles (manager)
2018-12-17 14:00

I looked more closely the code generated by RTE... It is buggy because one cast is missing. See https://bts.frama-c.com/view.php?id=2419. I believe that the internal generated types are correct though. It would explain why all is fine when using -then (and -e-acsl-prepare), without printing and parsing the generated code.
(0006716)
rmalak (reporter)
2018-12-17 14:01
edited on: 2018-12-17 14:03

ok I'll stay with only a single target (RTE+E-ACSL) for the Makefile Thanks !

- Issue History
Date Modified Username Field Change
2018-12-03 18:31 rmalak New Issue
2018-12-03 18:31 rmalak Status new => assigned
2018-12-03 18:31 rmalak Assigned To => signoles
2018-12-03 18:31 rmalak File Added: boolean.c
2018-12-03 19:01 signoles Note Added: 0006687
2018-12-03 19:01 signoles Status assigned => confirmed
2018-12-03 19:49 rmalak Note Added: 0006688
2018-12-12 11:26 signoles Category Plug-in > RTE => Plug-in > E-ACSL
2018-12-13 17:39 rmalak Note Added: 0006707
2018-12-13 18:19 signoles Note Added: 0006708
2018-12-13 21:11 rmalak Note Added: 0006710
2018-12-14 09:30 signoles Note Added: 0006711
2018-12-14 11:10 rmalak Note Added: 0006712
2018-12-17 13:58 signoles Relationship added related to 0002419
2018-12-17 14:00 signoles Note Added: 0006715
2018-12-17 14:01 rmalak Note Added: 0006716
2018-12-17 14:02 rmalak Note Edited: 0006716 View Revisions
2018-12-17 14:03 rmalak Note Edited: 0006716 View Revisions
2018-12-17 14:03 rmalak Note Edited: 0006716 View Revisions


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker