diffblue/cbmc

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.