Build failure if only the eva plugin is selected: -rectypes is required
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 thenmake
, it builds fine, because in the first make invocation the .cmo is not in the dependency tree, so -rectypes won't be added.