<!-- Thank you for submitting an issue to the Frama-C team. We propose the following template to ease the process. Please directly edit it inline to provide the required information. Before submitting the issue, please verify: - the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues); - you installed Frama-C as prescribed in the [instructions](INSTALL.md). If the issue applies to a specific Frama-C plug-in, please prefix the title by the plug-in name: [Eva], [WP], [E-ACSL]… --> ### Steps to reproduce the issue <!-- Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue. --> Instrument the following code with E-ACSL: ``` typedef struct test_enum test_enum; struct test_enum { int field_1; }; static test_enum const CURRENT_TEST = {.field_1 = (int)1}; int main(){ int test; /*@ assert \valid(&CURRENT_TEST.field_1);*/ /*@ assert \separated(&CURRENT_TEST.field_1, &test);*/ } ``` Please note that either of those assertions trigger the issue, and that the problem did not occur in Frama-C versions prior to 32.0/Germanium . ### Expected behaviour Frama-C/E-ACSL generates the instrumented/monitored code. ### Actual behaviour Frama-C/E-ACSL crashes with the following error: ``` [kernel] Parsing enum_crash.c (with preprocessing) [e-acsl] beginning translation. [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [kernel] Current source was: <unknown> The full backtrace is: Raised at Frama_c_kernel__Project.on in file "src/libraries/project/project.ml", line 357, characters 59-66 Called from E_ACSL__Main.generate_code.(fun) in file "src/plugins/e-acsl/src/main.ml", line 32, characters 7-1023 Called from Frama_c_kernel__State_builder.Hashtbl.memo in file "src/libraries/project/state_builder.ml", line 574, characters 17-22 Called from E_ACSL__Main.main in file "src/plugins/e-acsl/src/main.ml", line 164, characters 11-56 Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15 Called from Frama_c_kernel__Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 24, characters 4-17 Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 981, characters 2-9 Called from Frama_c_kernel__Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 1037, characters 18-64 Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8 Unexpected error (Invalid_argument("path should not be empty")). Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues Your Frama-C version is 32.0 (Germanium). Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs ``` It maybe interesting to note that I've encountered this issue on a very large code base; from the looks of it, and given instrumentation times, I have the feeling that E-ACSL does still perform the whole instrumentation, and crashes right before outputting the expected monitored code ? ### Contextual information - Frama-C installation mode: *Opam* - Frama-C version: *32.0 (Germanium)* (tested in 30, 31 and 32, crash observed in 32.0 only) - Plug-in used: *E-ACSL* - OS name: *Ubuntu* - OS version: *22.04.5 LTS* ### Additional information (optional) FYI @nkosmatov <!-- You may add here any information deemed relevant with regard to this issue, and tell us if you already tried some workarounds or have some ideas to solve this issue. -->