Closed
Description
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.