Xen integration test compilation fails
Opened this issue · 1 comments
CBMC version: 6.0.0-preview (cbmc-6.0.0-alpha-225-g40a981fbb8)
Operating system: Ubuntu 22.04
Exact command line resulting in the issue: cd integration/xen; make
What behaviour did you expect:
The integration test should create a docker image from the Dockerfile, start the docker container, and compile Xen with goto-cc
What happened instead:
The step that creates a docker image from the Dockerfile fails to compile CBMC, i.e., it is failing at line 8 of the docker_compile_xen.sh script
The compilation error is:
g++ -o goto-inspect -Wl,--start-group ../big-int/big-int.a ../linking/linking.a ../langapi/langapi.a ../goto-programs/goto-programs.a ../util/util.a goto_inspect_main.o goto_inspect_parse_options.o -Wl,--end-group
g++ -o goto-cc -Wl,--start-group ../big-int/big-int.a ../goto-programs/goto-programs.a ../util/util.a ../linking/linking.a ../ansi-c/ansi-c.a ../cpp/cpp.a ../xmllang/xmllang.a ../assembler/assembler.a ../langapi/langapi.a ../json/json.a armcc_cmdline.o armcc_mode.o as86_cmdline.o as_cmdline.o as_mode.o bcc_cmdline.o cl_message_handler.o compile.o cw_mode.o gcc_cmdline.o gcc_message_handler.o gcc_mode.o goto_cc_cmdline.o goto_cc_languages.o goto_cc_main.o goto_cc_mode.o hybrid_binary.o ld_cmdline.o ld_mode.o linker_script_merge.o ms_cl_cmdline.o ms_cl_mode.o ms_cl_version.o ms_link_cmdline.o ms_link_mode.o -Wl,--end-group
In file included from ../util/message.h:20:0,
from ../solvers/prop/prop.h:15,
from sat/cnf.h:15,
from sat/satcheck_minisat2.h:13,
from sat/satcheck_minisat2.cpp:9:
../util/source_location.h:16:20: fatal error: optional: No such file or directory
compilation terminated.
make[1]: *** [sat/satcheck_minisat2.o] Error 1
make[1]: *** Waiting for unfinished jobs....
CBMC compiles correctly outside of the docker container. I am using Docker version 20.10.17, build 100c701.
I believe the fix is to update https://github.com/diffblue/cbmc/blob/develop/integration/xen/Dockerfile#L1: we need to move to a Ubuntu release that has a reasonably current compiler. Ubuntu 16.04 doesn't quite do it anymore.