GitLab

Steps to reproduce the issue

• untar the frama-c-24.0 sources
• configure with: --disable-landmarks --with-no-plugin --enable-gui --enable-callgraph --enable-server --enable-eva
• make

Expected behaviour

Compilation succeeds

Actual behaviour

Compilation fails with the following message:

Ocamlc       src/plugins/value/domains/multidim_domain.cmo
File "src/plugins/value/domains/multidim_domain.ml", line 1:
Error: Invalid import of Abstract_memory, which uses recursive types.
       The compilation flag -rectypes is required
make: *** [share/Makefile.generic:78: src/plugins/value/domains/multidim_domain.cmo] Error 2

Contextual information

• Frama-C installation mode: from source
• Frama-C version: 24.0
• Plug-in used: Eva (and dependencies)
• OS name: Linux
• OS version: Gentoo linux

Additional information (optional)

• With no configure options, it builds fine.
• I've tried to debug the issue, and I think this is caused by having "-rectypes" added to BFLAGS for the rule compiling src/kernel_services/abstract_interp/abstract_memory.mli; which seems to be added as a side effect of the following line in the Makefile:

src/kernel_services/abstract_interp/abstract_memory.cmo: BFLAGS += -rectypes

For some reason, the dependency tree happens to change between the two configurations (default ./configure and ./configure with the aforementioned options), and in the latter case, the .cmi is a dependency of the .cmo, and thus inherits the local variables including BFLAGS.

• If I run make src/kernel_services/abstract_interp/abstract_memory.cmi and then make, it builds fine, because in the first make invocation the .cmo is not in the dependency tree, so -rectypes won't be added.