Skip to content

Xen integration test compilation fails #8193

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
polgreen opened this issue Feb 6, 2024 · 1 comment · Fixed by #8381
Closed

Xen integration test compilation fails #8193

polgreen opened this issue Feb 6, 2024 · 1 comment · Fixed by #8381

Comments

@polgreen
Copy link
Contributor

polgreen commented Feb 6, 2024

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.

@tautschnig
Copy link
Collaborator

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.

tautschnig added a commit to tautschnig/cbmc that referenced this issue Jul 12, 2024
Ubuntu 16.04 does not have a sufficiently recent compiler to build CBMC.
Use a more modern release and update packages as needed.

Fixes: diffblue#8193
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants