Frama-C WP crashes with Invalid_argument("Invalid lock on mutex") when trying to use Coq
I'm currently working on a file with WP and RTE where, sometimes, frama-c will crash when using the option -wp-prover why3:coq -wp-interactive fix
. Note that CVC4, AltErgo and Z3 are also used but disabling them doesn't have an effect. The crash happens right after an editor (Emacs with ProofGeneral in my case, but it also happens with CoqIDE) is opened: the editor closes nearly immediately and Frama-C produces the stacktrace below. Modifying the file slightly (e.g. by adding an extra assertion somewhere) will sometime stop Frama-C from crashing, however I can't seem to find a pattern. I'm currently running C-Reduce on my file to extract a MWE, I will post it in the comments as soon as it terminates (if it produces something useful). See below for information on my setup.
I'm wondering if anyone as an idea as to what causes this behaviour and if it can be fixed easily?
[kernel] Current source was: FRAMAC_SHARE/libc/stdlib.h:626
The full backtrace is:
Raised at Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 268, characters 41-48
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 269, characters 2-12
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 269, characters 2-12
Called from Stdlib__queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (Invalid_argument("Invalid lock on mutex")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 23.1 (Vanadium).
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
Contextual informations
- Frama-C installation method: opam
- Frama-C version: 23.1
- Plug-in used: WP + RTE
- OS Name: Fedora
- OS Version: 34
- Coq Version: 8.13.2
- Why3 Version: 1.4.0