Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Lablgtk-based GUI crashes with OCaml 4.03+beta1 #7162
Original bug ID: 7162
The Frama-C GUI, based on lablgtk, currently crashes when compiled with OCaml 4.03+beta1: a segmentation fault is produced in the Gtk code.
Here's the end of the backtrace:
Program received signal SIGSEGV, Segmentation fault.
The last line is part of the Frama-C code.
I believe there might be several different factors contributing to this bug, but so far, after a manual bisection, I ended up at commit 8851e6b (Allow allocating custom blocks with finalizers in the minor heap.). The preceding commit (ceb5e0b) does not crash.
[ocaml] (use Sys.enable_runtime_warnings to control these warnings)
I had never seen these messages before, and they likely appear with several other commits. The named files are temporary files produced by Frama-C, which indicates that there might also be a bug in our code base. In the end, I think that there is an influence of several previously unnoticed bugs.
Steps to reproduce
Note: it seems that it is not possible to install lablgtk directly from the stable versions of camlp4, so I preprocessed the lablgtk files and removed the camlp4 dependence. With the attached archive (which includes a "opam" file), it should be possible to locally do a
I'll later try to add the (approximate) sequence of commands necessary to reproduce the entire installation.
Comment author: @garrigue
Seeing the name of the commit, this is not too surprising.
Comment author: dobenour
I think that this is simply a bug in LablGTK -- in fact, I think that assuming that any block in the OCaml heap does not move is a bug. LablGTK needs to be fixed to use a registered GC root to access all OCaml objects. If this is too expensive, a single root could hold a reference to an array of Obj.t that is resized when needed, and the references could be replaced by integers.
The other solution would be for OCaml to provide an API to allocate blocks in the C heap together with counterparts in the OCaml heap.
Comment author: @garrigue
Can you try to apply the alloc_custom.diff patch to lablgtk and/or use the git version (either ocamlforge or github, they are the same)?
If somebody had the courage to track down the places where it is required to remove them, this could be a better solution, but it is so easy to break something that works...
Comment author: maro
I've updated my 4.03 branch to commit 95410ef and then applied your patch, and it works without problems.
I performed several tests and did not get any crashes or issues related to lablgtk.
I did not test 100% of our GUI, but I do believe every major component has been tested.
Thank you for the investigation and the patch!