Skip to content

Compiling with experimental BDD guards fails #7726

Closed
@martinlester

Description

@martinlester

CBMC version: 5.83.0
Operating system: Debian 12
Exact command line resulting in the issue: cmake -S . -Bbuild -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" ; cmake --build build
What behaviour did you expect: Successful compilation.
What happened instead: Compilation error.

[ 53%] Building CXX object src/goto-instrument/CMakeFiles/goto-instrument-lib.dir/goto_instrument_parse_options.cpp.o
/home/mariusz/tmp/cbmc-cbmc-5.83.0/src/goto-instrument/goto_instrument_parse_options.cpp: In member function ‘virtual int goto_instrument_parse_optionst::doit()’:
/home/mariusz/tmp/cbmc-cbmc-5.83.0/src/goto-instrument/goto_instrument_parse_options.cpp:876:22: error: aggregate ‘guard_managert guard_manager’ has incomplete type and cannot be defined
  876 |       guard_managert guard_manager;
      |                      ^~~~~~~~~~~~~
gmake[2]: *** [src/goto-instrument/CMakeFiles/goto-instrument-lib.dir/build.make:1056: src/goto-instrument/CMakeFiles/goto-instrument-lib.dir/goto_instrument_parse_options.cpp.o] Error 1
gmake[1]: *** [CMakeFiles/Makefile2:3227: src/goto-instrument/CMakeFiles/goto-instrument-lib.dir/all] Error 2
gmake: *** [Makefile:166: all] Error 2

I can make it compile by changing the include in src/analyses/guard_bdd.h from <solvers/bdd/bdd.h> to <solvers/prop/bdd_expr.h>.

But I'm not 100% sure that's the correct thing to do. Comments suggest there's the potential for something subtle to go wrong if code from the wrong BDD implementation is included, and I don't know the codebase well enough to tell if that would happen here.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions