Skip to content

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 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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information