From 69500144447a99445c40a64ddeb269ad094b1fda Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Feb 2024 10:09:47 +0000 Subject: [PATCH] Add support for GNU Hurd Builds with tests passing on hurd-i386 per https://buildd.debian.org/status/fetch.php?pkg=cbmc&arch=hurd-i386&ver=5.95.1-6&stamp=1714528231&raw=0. --- doc/man/cbmc.1 | 2 +- doc/man/goto-analyzer.1 | 2 +- doc/man/janalyzer.1 | 2 +- doc/man/jbmc.1 | 2 +- src/goto-cc/hybrid_binary.cpp | 3 ++- src/util/config.cpp | 4 +++- src/util/config.h | 2 +- 7 files changed, 10 insertions(+), 7 deletions(-) diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index f27bf308c17..6798f463eb9 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -202,7 +202,7 @@ Set analysis architecture, which defaults to the host architecture. Use one of: \fB\-\-os\fR \fIos\fR Set analysis operating system, which defaults to the host operating system. Use one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR, -\fBsolaris\fR, or \fBwindows\fR. +\fBsolaris\fR, \fBhurd\fR, or \fBwindows\fR. .TP \fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR Set analysis architecture and operating system. diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1 index 7db47a91086..d1e19309640 100644 --- a/doc/man/goto-analyzer.1 +++ b/doc/man/goto-analyzer.1 @@ -461,7 +461,7 @@ Set analysis architecture, which defaults to the host architecture. Use one of: \fB\-\-os\fR \fIos\fR Set analysis operating system, which defaults to the host operating system. Use one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR, -\fBsolaris\fR, or \fBwindows\fR. +\fBsolaris\fR, \fBhurd\fR, or \fBwindows\fR. .TP \fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR Set analysis architecture and operating system. diff --git a/doc/man/janalyzer.1 b/doc/man/janalyzer.1 index 283cf84be5f..c6676676c6f 100644 --- a/doc/man/janalyzer.1 +++ b/doc/man/janalyzer.1 @@ -279,7 +279,7 @@ Set analysis architecture, which defaults to the host architecture. Use one of: \fB\-\-os\fR \fIos\fR Set analysis operating system, which defaults to the host operating system. Use one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR, -\fBsolaris\fR, or \fBwindows\fR. +\fBsolaris\fR, \fBhurd\fR, or \fBwindows\fR. .TP \fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR Set analysis architecture and operating system. diff --git a/doc/man/jbmc.1 b/doc/man/jbmc.1 index ae413c6308c..935098eb125 100644 --- a/doc/man/jbmc.1 +++ b/doc/man/jbmc.1 @@ -83,7 +83,7 @@ Set analysis architecture, which defaults to the host architecture. Use one of: \fB\-\-os\fR \fIos\fR Set analysis operating system, which defaults to the host operating system. Use one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR, -\fBsolaris\fR, or \fBwindows\fR. +\fBsolaris\fR, \fBhurd\fR, or \fBwindows\fR. .TP \fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR Set analysis architecture and operating system. diff --git a/src/goto-cc/hybrid_binary.cpp b/src/goto-cc/hybrid_binary.cpp index ab51fcbf955..1bd529c872f 100644 --- a/src/goto-cc/hybrid_binary.cpp +++ b/src/goto-cc/hybrid_binary.cpp @@ -49,7 +49,8 @@ int hybrid_binary( int result = 0; #if defined(__linux__) || defined(__FreeBSD_kernel__) || \ - defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__) + defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__) || \ + defined(__gnu_hurd__) // we can use objcopy for both object files and executables (void)building_executable; diff --git a/src/util/config.cpp b/src/util/config.cpp index c853ffa582a..c0c999c4cc0 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -985,7 +985,7 @@ bool configt::set(const cmdlinet &cmdline) ansi_c.mode = ansi_ct::flavourt::CLANG; ansi_c.preprocessor=ansi_ct::preprocessort::CLANG; } - else if(os == "linux" || os == "solaris" || os == "netbsd") + else if(os == "linux" || os == "solaris" || os == "netbsd" || os == "hurd") { ansi_c.lib=configt::ansi_ct::libt::LIB_FULL; ansi_c.os=configt::ansi_ct::ost::OS_LINUX; @@ -1509,6 +1509,8 @@ irep_idt configt::this_operating_system() this_os="linux"; #elif __SVR4 this_os="solaris"; +#elif __gnu_hurd__ + this_os = "hurd"; #else this_os="unknown"; #endif diff --git a/src/util/config.h b/src/util/config.h index fdf15fbf270..f7bc65c6033 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -107,7 +107,7 @@ class symbol_table_baset; "set operating system (default: " + \ id2string(configt::this_operating_system()) + \ ") to one of: {yfreebsd}, {ylinux}, {ymacos}, {ynetbsd}, {yopenbsd}, " \ - "{ysolaris}, or {ywindows}\n" \ + "{ysolaris}, {yhurd}, or {ywindows}\n" \ " {y--i386-linux}, {y--i386-win32}, {y--i386-macos}, {y--ppc-macos}, " \ "{y--win32}, {y--winx64} \t " \ "set architecture and operating system\n" \