Stack overflow using WP in Wp__Register.step_finally
Frama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
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 in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 880, characters 18-64
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).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.1 (Iron).
The function to be proved is part of a rather big C file included in the attached archive. Sorry for the complexity (and maybe the bad quality) of the C code, it is in fact produced by a Lustre compiler we are working on. I will try to produce a real MWE...
Running Frama-C and WP on the whole file causes a stack overflow on List.map
but I reduce the error when proving the Arrays1_Arrays1_node_step
function. I use the ref
and the real
memory model.
When launching Frama-C on the function, no goal is produced (at least there is no printing of it), only Frama-C is running (there is no process involving Alt-Ergo or Z3 for instance). the crash happens after 13 minutes (!) on my computer (a recent laptop with i9 cores).
Steps to reproduce the issue
- open the attached archive
- issue the following command:
frama-c -wp -wp-model ref,real -wp-fct Arrays1_Arrays1_node_step Arrays1.c
Contextual information
- Frama-C installation mode: opam with an OCaml 4.14.0 switch
- Frama-C version: 26.1 (Iron)
- Plug-in used: WP
- OS name: Linux
- OS version: 22.04
Thanks,
Christophe