With 4.08 (including the 4.08.1+rc1), we have an issue with the bytecode version of Frama-C, where the dynamic loading of modules (via Dynlink) no longer works as before, with error messages such as "no implementation available for ".
A quick glance through the changelog did not indicate a likely culprit. We had a typing issue related to -pack which has already been solved in our development version, but this bug might be unrelated, since we can now type, compile and run Frama-C in native version without issues.
For a more concrete description, here's an example of what happens when trying to run frama-c.byte after compiling it, in 4.08 (among several similar messages):
[kernel] User Error: cannot load plug-in 'Callgraph': cannot load module
Details: no implementation available for Callgraph.Options
Callgraph.cmo is produced by packing several modules, including an options.cmo. This compiles, both in bytecode and in native version, and when running the native version of Frama-C (which loads the corresponding .cmxs file), everything works fine. However, when running the bytecode version (frama-c.byte), these errors appear. Both versions work fine up to 4.07. (I could not test with 4.09 since we depend on dune, but I assume no changes related to it.)
We can try to produce a minimal, self-contained version, but it could take some time. Do you have an idea of something else we could do to further debug this issue?
The text was updated successfully, but these errors were encountered:
The mistake is in #2176 which treats Symtable.required_globals as if all persistent identifiers returned by it will be toplevel modules, which is not true for a packed cmo file where it will also contain sub-modules.
The fix is just to ignore identifiers with "." in their name when creating the list of implementation_imports in the bytecode implementation of dynlink.ml. I'll make a PR this afternoon.