Stack overflow during e-acsl translation of runtime error assertions on coreutils program
I'm trying to leverage frama-c rte and e-acsl plugins to encode all runtime errors through assertions, following "A Lesson on Runtime Assertion Checking with Frama-C". I might have gotten a bit ambitious and tried to launch it on some preprocessed coreutils file.
Steps to reproduce the issue
Attached is chcon_comb2.c.
$ frama-c -rte chcon_comb2.c -machdep x86_64 -then -e-acsl -then-on e-ascl -print -ocode chcon_comb2_rte.c
[...]
Ignoring annotation.
[kernel] Current source was: chcon_comb2.c:48883
The full backtrace is:
Raised at Frama_c_kernel__Project.on in file "src/libraries/project/project.ml", line 365, characters 59-66
Called from E_ACSL__Main.generate_code.(fun) in file "src/plugins/e-acsl/src/main.ml", line 46, characters 7-1023
Called from Frama_c_kernel__State_builder.Hashtbl.memo in file "src/libraries/project/state_builder.ml", line 569, characters 17-22
Called from E_ACSL__Main.main in file "src/plugins/e-acsl/src/main.ml", line 162, characters 11-56
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Frama_c_boot__Boot.play_analysis in file "src/init/boot/boot.ml", line 36, characters 4-20
Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 850, characters 2-9
Called from Frama_c_kernel__Cmdline.play_in_toplevel.aux in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 865, characters 30-76
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8
Unexpected error (Stack overflow).
Expected behaviour
I was wondering if there was an easy fix in the source code to avoid this Stack overflow?
As a side note, the rte package seems to not support "Builtins for long double type". For now I just changed the types.
Contextual information
- Frama-C installation mode: opam
- Frama-C version: 27.0 (Cobalt)
- Plug-in used: RTE & E-ACSL
- OS name: Ubuntu
- OS version: 22.04.2