Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2593

Closed
Open
Created Jan 13, 2022 by fx-carton@fx-carton

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
Assignee
Assign to
Time tracking