Skip to content

Commit 724a95a

Browse files
tautschnigtautschnig
committed
Also build and test OpenBSD, NetBSD
Uses the same virtualisation set-up as FreeBSD checks.
1 parent c37bd7a commit 724a95a

File tree

11 files changed

+157
-24
lines changed

11 files changed

+157
-24
lines changed

‎.github/workflows/bsd.yaml‎

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,3 +66,126 @@ jobs:
6666
# gmake -C regression/cbmc test-paths-lifo
6767
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
6868
# # gmake -C jbmc/regression test-parallel JOBS=2
69+
70+
# This job takes approximately X to 34 minutes
71+
OpenBSD:
72+
runs-on: ubuntu-latest
73+
steps:
74+
- uses: actions/checkout@v3
75+
with:
76+
submodules: recursive
77+
- name: Prepare ccache
78+
uses: actions/cache@v3
79+
with:
80+
path: .ccache
81+
key: openbsd-7.4-gmake-${{ github.ref }}-${{ github.sha }}-PR
82+
restore-keys: |
83+
openbsd-7.4-gmake-${{ github.ref }}
84+
openbsd-7.4-gmake
85+
- name: ccache environment
86+
run: |
87+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
88+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
89+
- name: Build and Test
90+
uses: cross-platform-actions/action@v0.21.1
91+
with:
92+
operating_system: openbsd
93+
version: '7.4'
94+
hypervisor: qemu
95+
run: |
96+
echo "Fetch dependencies"
97+
sudo pkg_add -v bash gmake llvm%16 git python3 bison ccache parallel z3
98+
sudo ln -s $(which llvm-ar-16) /usr/local/bin/llvm-ar
99+
echo "Fetch JBMC dependencies"
100+
sudo pkg_add -v jdk%1.8 wget maven
101+
echo "Zero ccache stats and limit in size"
102+
export CCACHE_BASEDIR=$PWD
103+
export CCACHE_DIR=$PWD/.ccache
104+
ccache -z --max-size=500M
105+
ccache -p
106+
echo "Build with gmake"
107+
gmake -C src minisat2-download
108+
# we only build util.a to keep job execution time in check
109+
gmake -C src -j2 CXX="ccache clang++" util.dir
110+
# # don't do JBMC so as to keep the overall time in check
111+
# gmake -C src -j2 CXX="ccache clang++"
112+
# # gmake -C jbmc/src setup-submodules
113+
# # gmake -C jbmc/src -j2 CXX="ccache clang++"
114+
# gmake -C unit "CXX=ccache clang++"
115+
# # gmake -C jbmc/unit "CXX=ccache clang++"
116+
# echo "Print ccache stats"
117+
# ccache -s
118+
# echo "Checking completeness of help output"
119+
# scripts/check_help.sh clang++
120+
# echo "Run unit tests"
121+
# gmake -C unit test
122+
# # gmake -C jbmc/unit test
123+
# echo "Running expected failure tests"
124+
# gmake TAGS='[!shouldfail]' -C unit test
125+
# # gmake TAGS='[!shouldfail]' -C jbmc/unit test
126+
# echo "Run regression tests"
127+
# gmake -C regression test-parallel JOBS=2
128+
# gmake -C regression/cbmc test-paths-lifo
129+
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
130+
# # gmake -C jbmc/regression test-parallel JOBS=2
131+
132+
# This job takes approximately X to 21 minutes
133+
NetBSD:
134+
runs-on: ubuntu-latest
135+
steps:
136+
- uses: actions/checkout@v3
137+
with:
138+
submodules: recursive
139+
- name: Prepare ccache
140+
uses: actions/cache@v3
141+
with:
142+
path: .ccache
143+
key: netbsd-9.3-gmake-${{ github.ref }}-${{ github.sha }}-PR
144+
restore-keys: |
145+
netbsd-9.3-gmake-${{ github.ref }}
146+
netbsd-9.3-gmake
147+
- name: ccache environment
148+
run: |
149+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
150+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
151+
- name: Build and Test
152+
uses: cross-platform-actions/action@v0.21.1
153+
with:
154+
operating_system: netbsd
155+
version: '9.3'
156+
hypervisor: qemu
157+
run: |
158+
echo "Fetch dependencies"
159+
export PATH=/usr/pkg/sbin:/usr/pkg/bin:$PATH
160+
export PKG_PATH=https://cdn.netbsd.org/pub/pkgsrc/packages/NetBSD/amd64/9.3/All/
161+
sudo pkgin -y install bash gmake git python311 patch flex bison ccache parallel z3
162+
sudo ln -s $(which python3.11) /usr/pkg/bin/python3
163+
echo "Fetch JBMC dependencies"
164+
sudo pkgin -y install openjdk8 wget apache-maven
165+
echo "Zero ccache stats and limit in size"
166+
export CCACHE_BASEDIR=$PWD
167+
export CCACHE_DIR=$PWD/.ccache
168+
ccache -z --max-size=500M
169+
ccache -p
170+
echo "Build with gmake"
171+
gmake -C src minisat2-download
172+
# we only build util.a to keep job execution time in check
173+
gmake -C src -j2 CXX="ccache g++" util.dir
174+
# # don't do JBMC so as to keep the overall time in check
175+
# gmake -C src -j2 CXX="ccache g++"
176+
# # gmake -C jbmc/src setup-submodules
177+
# # gmake -C jbmc/src -j2 CXX="ccache g++"
178+
# gmake -C unit "CXX=ccache g++"
179+
# # gmake -C jbmc/unit "CXX=ccache g++"
180+
# echo "Print ccache stats"
181+
# ccache -s
182+
# echo "Checking completeness of help output"
183+
# scripts/check_help.sh g++
184+
# echo "Run unit tests"
185+
# # ignore failures for the moment
186+
# gmake -C unit test
187+
# # gmake -C jbmc/unit test
188+
# echo "Running expected failure tests"
189+
# gmake TAGS='[!shouldfail]' -C unit test
190+
# # gmake TAGS='[!shouldfail]' -C jbmc/unit test
191+
# echo "Run regression tests"

‎doc/man/cbmc.1‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -201,8 +201,8 @@ Set analysis architecture, which defaults to the host architecture. Use one of:
201201
.TP
202202
\fB\-\-os\fR \fIos\fR
203203
Set analysis operating system, which defaults to the host operating system. Use
204-
one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
205-
\fBwindows\fR.
204+
one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR,
205+
\fBsolaris\fR, or \fBwindows\fR.
206206
.TP
207207
\fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
208208
Set analysis architecture and operating system.

‎doc/man/goto-analyzer.1‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -460,8 +460,8 @@ Set analysis architecture, which defaults to the host architecture. Use one of:
460460
.TP
461461
\fB\-\-os\fR \fIos\fR
462462
Set analysis operating system, which defaults to the host operating system. Use
463-
one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
464-
\fBwindows\fR.
463+
one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR,
464+
\fBsolaris\fR, or \fBwindows\fR.
465465
.TP
466466
\fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
467467
Set analysis architecture and operating system.

‎doc/man/janalyzer.1‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -278,8 +278,8 @@ Set analysis architecture, which defaults to the host architecture. Use one of:
278278
.TP
279279
\fB\-\-os\fR \fIos\fR
280280
Set analysis operating system, which defaults to the host operating system. Use
281-
one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
282-
\fBwindows\fR.
281+
one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR,
282+
\fBsolaris\fR, or \fBwindows\fR.
283283
.TP
284284
\fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
285285
Set analysis architecture and operating system.

‎doc/man/jbmc.1‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -82,8 +82,8 @@ Set analysis architecture, which defaults to the host architecture. Use one of:
8282
.TP
8383
\fB\-\-os\fR \fIos\fR
8484
Set analysis operating system, which defaults to the host operating system. Use
85-
one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBsolaris\fR, or
86-
\fBwindows\fR.
85+
one of: \fBfreebsd\fR, \fBlinux\fR, \fBmacos\fR, \fBnetbsd\fR, \fBopenbsd\fR,
86+
\fBsolaris\fR, or \fBwindows\fR.
8787
.TP
8888
\fB\-\-i386\-linux\fR, \fB\-\-i386\-win32\fR, \fB\-\-i386\-macos\fR, \fB\-\-ppc\-macos\fR, \fB\-\-win32\fR, \fB\-\-winx64\fR
8989
Set analysis architecture and operating system.

‎src/big-int/allocainc.h‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,9 +49,10 @@ extern "C" void *alloca (unsigned);
4949

5050
# define alloca(X) __builtin_alloca(X)
5151

52-
#elif defined __FreeBSD__ || defined __FreeBSD_kernel__ || defined __OpenBSD__
52+
#elif defined __FreeBSD__ || defined __FreeBSD_kernel__ || \
53+
defined __OpenBSD__ || defined __NetBSD__
5354

54-
# include <stdlib.h>
55+
# include <stdlib.h>
5556

5657
#endif
5758

‎src/common‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,10 @@ else ifeq ($(uname),Darwin)
99
BUILD_ENV_ := OSX
1010
else ifeq ($(uname),FreeBSD)
1111
BUILD_ENV_ := FreeBSD
12+
else ifeq ($(uname),OpenBSD)
13+
BUILD_ENV_ := OpenBSD
14+
else ifeq ($(uname),NetBSD)
15+
BUILD_ENV_ := NetBSD
1216
else ifeq ($(filter-out MINGW32_%, $(uname)),)
1317
BUILD_ENV_ := MinGW
1418
else ifeq ($(filter-out CYGWIN_%, $(uname)),)
@@ -20,7 +24,7 @@ else
2024
BUILD_ENV_ := $(BUILD_ENV)
2125
endif
2226

23-
ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD,$(BUILD_ENV_)),)
27+
ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD OpenBSD NetBSD,$(BUILD_ENV_)),)
2428
# Linux-ish
2529
LIBEXT = .a
2630
OBJEXT = .o
@@ -62,7 +66,7 @@ ifeq ($(filter-out OSX OSX_Universal,$(BUILD_ENV_)),)
6266
CXX = clang++
6367
endif
6468
YFLAGS ?= -v
65-
else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),)
69+
else ifeq ($(filter-out FreeBSD OpenBSD,$(BUILD_ENV_)),)
6670
CP_CXXFLAGS +=
6771
LINKLIB = llvm-ar rcT $@ $^
6872
LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)

‎src/goto-cc/gcc_mode.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ static std::string compiler_name(
5959
base_name=="goto-gcc" ||
6060
base_name=="goto-ld")
6161
{
62-
#ifdef __FreeBSD__
62+
#if defined(__FreeBSD__) || defined(__OpenBSD__)
6363
return "clang";
6464
#else
6565
return "gcc";

‎src/goto-cc/hybrid_binary.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ int hybrid_binary(
4949
int result = 0;
5050

5151
#if defined(__linux__) || defined(__FreeBSD_kernel__) || \
52-
defined(__FreeBSD__) || defined(__OpenBSD__)
52+
defined(__FreeBSD__) || defined(__OpenBSD__) || defined(__NetBSD__)
5353
// we can use objcopy for both object files and executables
5454
(void)building_executable;
5555

‎src/util/config.cpp‎

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -934,13 +934,13 @@ bool configt::set(const cmdlinet &cmdline)
934934
#ifdef _WIN32
935935
ansi_c.preprocessor=ansi_ct::preprocessort::VISUAL_STUDIO;
936936
ansi_c.mode=ansi_ct::flavourt::VISUAL_STUDIO;
937-
#elif __FreeBSD__
937+
#elif defined(__FreeBSD__) || defined(__OpenBSD__)
938938
ansi_c.preprocessor=ansi_ct::preprocessort::CLANG;
939939
ansi_c.mode=ansi_ct::flavourt::VISUAL_STUDIO;
940-
#else
940+
#else
941941
ansi_c.preprocessor=ansi_ct::preprocessort::GCC;
942942
ansi_c.mode=ansi_ct::flavourt::VISUAL_STUDIO;
943-
#endif
943+
#endif
944944

945945
cpp.cpp_standard = cppt::cpp_standardt::CPP14;
946946
}
@@ -952,14 +952,14 @@ bool configt::set(const cmdlinet &cmdline)
952952
ansi_c.mode = ansi_ct::flavourt::CLANG;
953953
ansi_c.preprocessor=ansi_ct::preprocessort::CLANG;
954954
}
955-
else if(os=="linux" || os=="solaris")
955+
else if(os == "linux" || os == "solaris" || os == "netbsd")
956956
{
957957
ansi_c.lib=configt::ansi_ct::libt::LIB_FULL;
958958
ansi_c.os=configt::ansi_ct::ost::OS_LINUX;
959959
ansi_c.mode=ansi_ct::flavourt::GCC;
960960
ansi_c.preprocessor=ansi_ct::preprocessort::GCC;
961961
}
962-
else if(os=="freebsd")
962+
else if(os == "freebsd" || os == "openbsd")
963963
{
964964
ansi_c.lib=configt::ansi_ct::libt::LIB_FULL;
965965
ansi_c.os=configt::ansi_ct::ost::OS_LINUX;
@@ -1458,13 +1458,17 @@ irep_idt configt::this_operating_system()
14581458
this_os="macos";
14591459
#elif __FreeBSD__
14601460
this_os="freebsd";
1461-
#elif __linux__
1461+
#elif __OpenBSD__
1462+
this_os = "openbsd";
1463+
#elif __NetBSD__
1464+
this_os = "netbsd";
1465+
#elif __linux__
14621466
this_os="linux";
1463-
#elif __SVR4
1467+
#elif __SVR4
14641468
this_os="solaris";
1465-
#else
1469+
#else
14661470
this_os="unknown";
1467-
#endif
1471+
#endif
14681472

14691473
return this_os;
14701474
}

0 commit comments

Comments
 (0)