Skip to content

Commit 3ff2cf7

Browse files
tautschnigtautschnig
authored
Merge pull request #7924 from tautschnig/bugfixes/freebsd-build
Build and infrastructure fixes for FreeBSD
2 parents 8fc41f3 + 18a35b8 commit 3ff2cf7

File tree

86 files changed

+545
-129
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

86 files changed

+545
-129
lines changed

‎.githooks/pre-commit‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#!/bin/bash
1+
#!/usr/bin/env bash
22
# Runs scripts/cpplint.py on the modified files
33
# Based on https://github.com/s0enke/git-hooks/
44
#

‎.github/workflows/bsd.yaml‎

Lines changed: 193 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,193 @@
1+
name: Build and Test on *BSD
2+
on:
3+
push:
4+
branches: [ develop ]
5+
pull_request:
6+
branches: [ develop ]
7+
8+
jobs:
9+
# This job takes approximately 6 to 26 minutes
10+
FreeBSD:
11+
runs-on: ubuntu-latest
12+
steps:
13+
- uses: actions/checkout@v3
14+
with:
15+
submodules: recursive
16+
- name: Prepare ccache
17+
uses: actions/cache@v3
18+
with:
19+
path: .ccache
20+
key: freebsd-13.2-gmake-${{ github.ref }}-${{ github.sha }}-PR
21+
restore-keys: |
22+
freebsd-13.2-gmake-${{ github.ref }}
23+
freebsd-13.2-gmake
24+
- name: ccache environment
25+
run: |
26+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
27+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
28+
- name: Build and Test
29+
uses: vmactions/freebsd-vm@v1
30+
with:
31+
release: 13.2
32+
usesh: true
33+
run: |
34+
# apparently fail-on-error isn't the default here
35+
set -e -x
36+
echo "Fetch dependencies"
37+
pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3
38+
echo "Fetch JBMC dependencies"
39+
pkg install -y openjdk8 wget maven
40+
echo "Zero ccache stats and limit in size"
41+
export CCACHE_BASEDIR=$PWD
42+
export CCACHE_DIR=$PWD/.ccache
43+
ccache -z --max-size=500M
44+
ccache -p
45+
echo "Build with gmake"
46+
# don't do JBMC as to keep the overall time in check
47+
gmake -C src minisat2-download
48+
gmake -C src -j2 CXX="ccache clang++"
49+
# gmake -C jbmc/src setup-submodules
50+
# gmake -C jbmc/src -j2 CXX="ccache clang++"
51+
gmake -C unit "CXX=ccache clang++"
52+
# gmake -C jbmc/unit "CXX=ccache clang++"
53+
echo "Print ccache stats"
54+
ccache -s
55+
echo "Checking completeness of help output"
56+
scripts/check_help.sh clang++
57+
echo "Run unit tests"
58+
gmake -C unit test
59+
# gmake -C jbmc/unit test
60+
echo "Running expected failure tests"
61+
gmake TAGS='[!shouldfail]' -C unit test
62+
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
63+
echo "Run regression tests"
64+
gmake -C regression/cbmc test
65+
# gmake -C regression test-parallel JOBS=2
66+
# gmake -C regression/cbmc test-paths-lifo
67+
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
68+
# # gmake -C jbmc/regression test-parallel JOBS=2
69+
70+
# This job takes approximately 7 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: vmactions/openbsd-vm@v1
91+
with:
92+
release: 7.4
93+
run: |
94+
# apparently fail-on-error isn't the default here
95+
set -e -x
96+
echo "Fetch dependencies"
97+
pkg_add -v bash gmake llvm%16 git python3 bison ccache parallel z3
98+
ln -s $(which llvm-ar-16) /usr/local/bin/llvm-ar
99+
echo "Fetch JBMC dependencies"
100+
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+
# don't do JBMC so as to keep the overall time in check
108+
gmake -C src minisat2-download
109+
gmake -C src -j2 CXX="ccache clang++"
110+
# gmake -C jbmc/src setup-submodules
111+
# gmake -C jbmc/src -j2 CXX="ccache clang++"
112+
gmake -C unit "CXX=ccache clang++"
113+
# gmake -C jbmc/unit "CXX=ccache clang++"
114+
echo "Print ccache stats"
115+
ccache -s
116+
echo "Checking completeness of help output"
117+
scripts/check_help.sh clang++
118+
echo "Run unit tests"
119+
gmake -C unit test
120+
# gmake -C jbmc/unit test
121+
echo "Running expected failure tests"
122+
gmake TAGS='[!shouldfail]' -C unit test
123+
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
124+
echo "Run regression tests"
125+
gmake -C regression/cbmc test
126+
# gmake -C regression test-parallel JOBS=2
127+
# gmake -C regression/cbmc test-paths-lifo
128+
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
129+
# # gmake -C jbmc/regression test-parallel JOBS=2
130+
131+
# This job takes approximately 6 to 29 minutes
132+
NetBSD:
133+
runs-on: ubuntu-latest
134+
steps:
135+
- uses: actions/checkout@v3
136+
with:
137+
submodules: recursive
138+
- name: Prepare ccache
139+
uses: actions/cache@v3
140+
with:
141+
path: .ccache
142+
key: netbsd-9.3-gmake-${{ github.ref }}-${{ github.sha }}-PR
143+
restore-keys: |
144+
netbsd-9.3-gmake-${{ github.ref }}
145+
netbsd-9.3-gmake
146+
- name: ccache environment
147+
run: |
148+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
149+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
150+
- name: Build and Test
151+
uses: vmactions/netbsd-vm@v1
152+
with:
153+
release: 9.3
154+
run: |
155+
# apparently fail-on-error isn't the default here
156+
set -e -x
157+
echo "Fetch dependencies"
158+
pkg_add -v bash gmake git python311 patch flex bison ccache parallel z3 gcc10
159+
ln -s $(which python3.11) /usr/pkg/bin/python3
160+
export PATH=/usr/pkg/gcc10/bin:$PATH
161+
echo "Fetch JBMC dependencies"
162+
pkg_add -v openjdk8 wget apache-maven
163+
echo "Zero ccache stats and limit in size"
164+
export CCACHE_BASEDIR=$PWD
165+
export CCACHE_DIR=$PWD/.ccache
166+
ccache -z --max-size=500M
167+
ccache -p
168+
echo "Build with gmake"
169+
# don't do JBMC so as to keep the overall time in check
170+
gmake -C src minisat2-download
171+
gmake -C src -j2 CXX="ccache g++"
172+
# gmake -C jbmc/src setup-submodules
173+
# gmake -C jbmc/src -j2 CXX="ccache g++"
174+
gmake -C unit "CXX=ccache g++"
175+
# gmake -C jbmc/unit "CXX=ccache g++"
176+
echo "Print ccache stats"
177+
ccache -s
178+
echo "Checking completeness of help output"
179+
scripts/check_help.sh g++
180+
echo "Run unit tests"
181+
# TODO: unit tests are failing, requires debugging
182+
gmake -C unit test || true
183+
# gmake -C jbmc/unit test
184+
echo "Running expected failure tests"
185+
gmake TAGS='[!shouldfail]' -C unit test
186+
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
187+
echo "Run regression tests"
188+
# TODO: we need to model some more library functions
189+
gmake -C regression/cbmc test || true
190+
# gmake -C regression test-parallel JOBS=2
191+
# gmake -C regression/cbmc test-paths-lifo
192+
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
193+
# # gmake -C jbmc/regression test-parallel JOBS=2

‎.github/workflows/pull-request-check-clang-format.sh‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#!/bin/bash
1+
#!/usr/bin/env bash
22

33
# Stop on errors
44
set -e

‎.github/workflows/pull-request-check-cpplint.sh‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#!/bin/bash
1+
#!/usr/bin/env bash
22

33
# Stop on errors
44
set -e

‎.github/workflows/pull-request-checks.yaml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ jobs:
5959
- name: Print ccache stats
6060
run: ccache -s
6161
- name: Checking completeness of help output
62-
run: scripts/check_help.sh
62+
run: scripts/check_help.sh g++
6363
- name: Run unit tests
6464
run: |
6565
make -C unit test IPASIR=$PWD/riss.git/riss
@@ -247,7 +247,7 @@ jobs:
247247
- name: Print ccache stats
248248
run: ccache -s
249249
- name: Checking completeness of help output
250-
run: scripts/check_help.sh build/bin
250+
run: scripts/check_help.sh /usr/bin/g++ build/bin
251251
- name: Check if package building works
252252
run: |
253253
cd build

‎COMPILING.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ The environments below have been used successfully in the
1616
past, but are not actively tested:
1717

1818
- Solaris 11
19-
- FreeBSD 11
19+
- FreeBSD 13
2020

2121
# Building using CMake
2222

@@ -246,11 +246,11 @@ Maven 3 manually.
246246
247247
1. As root, get the necessary tools:
248248
```
249-
pkg install bash gmake git www/p5-libwww patch flex bison
249+
pkg install bash gmake git www/p5-libwww python python3 patch flex bison cvc5 z3
250250
```
251251
To compile JBMC, additionally install
252252
```
253-
pkg install openjdk8 wget maven3
253+
pkg install openjdk8 wget maven
254254
```
255255
2. As a user, get the CBMC source via
256256
```

‎doc/doxygen-root/doxygen-markdown/markdown.sh‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#!/bin/bash
1+
#!/usr/bin/env bash
22

33
set -euo pipefail
44

‎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.

0 commit comments

Comments
 (0)