Skip to content

Commit cb951fb

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #7496 from tautschnig/bugfixes/clang-14
Test builds using clang-14 in CI
2 parents 031ae2e + 4bd1d94 commit cb951fb

File tree

8 files changed

+172
-58
lines changed

8 files changed

+172
-58
lines changed

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

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -242,6 +242,76 @@ jobs:
242242
- name: Run tests
243243
run: cd build; ctest . -V -L CORE -j2
244244

245+
# This job takes approximately N minutes
246+
check-ubuntu-22_04-make-clang:
247+
runs-on: ubuntu-22.04
248+
env:
249+
CC: "ccache /usr/bin/clang"
250+
CXX: "ccache /usr/bin/clang++"
251+
steps:
252+
- uses: actions/checkout@v3
253+
with:
254+
submodules: recursive
255+
- name: Fetch dependencies
256+
env:
257+
# This is needed in addition to -yq to prevent apt-get from asking for
258+
# user input
259+
DEBIAN_FRONTEND: noninteractive
260+
run: |
261+
sudo apt-get update
262+
sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
263+
make -C src minisat2-download
264+
cpanm Thread::Pool::Simple
265+
- name: Confirm z3 solver is available and log the version installed
266+
run: z3 --version
267+
- name: Download cvc-5 from the releases page and make sure it can be deployed
268+
run: |
269+
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux
270+
chmod u+x cvc5
271+
mv cvc5 /usr/local/bin
272+
cvc5 --version
273+
- name: Prepare ccache
274+
uses: actions/cache@v3
275+
with:
276+
path: .ccache
277+
key: ${{ runner.os }}-22.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR
278+
restore-keys: |
279+
${{ runner.os }}-22.04-make-clang-${{ github.ref }}
280+
${{ runner.os }}-22.04-make-clang
281+
- name: ccache environment
282+
run: |
283+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
284+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
285+
- name: Zero ccache stats and limit in size
286+
run: ccache -z --max-size=500M
287+
- name: Perform C/C++ library syntax check
288+
run: |
289+
make -C src/ansi-c library_check
290+
make -C src/cpp library_check
291+
- name: Build with make
292+
run: |
293+
make -C src -j2
294+
make -C unit -j2
295+
make -C jbmc/src -j2
296+
make -C jbmc/unit -j2
297+
- name: Print ccache stats
298+
run: ccache -s
299+
- name: Run unit tests
300+
run: |
301+
make -C unit test
302+
make -C jbmc/unit test
303+
make TAGS="[z3]" -C unit test
304+
- name: Run expected failure unit tests
305+
run: |
306+
make TAGS="[!shouldfail]" -C unit test
307+
make TAGS="[!shouldfail]" -C jbmc/unit test
308+
- name: Run regression tests
309+
run: |
310+
make -C regression test-parallel JOBS=2
311+
make -C regression/cbmc test-paths-lifo
312+
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
313+
make -C jbmc/regression test-parallel JOBS=2
314+
245315
# This job takes approximately 41 minutes
246316
check-ubuntu-22_04-cmake-gcc:
247317
runs-on: ubuntu-22.04

‎src/ansi-c/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -109,7 +109,7 @@ else
109109
platform_unavail = library/java.io.c library/threads.c
110110
endif
111111
library_check: library/*.c
112-
./library_check.sh $(CC) $(filter-out $(platform_unavail), $^)
112+
./library_check.sh "$(CC)" $(filter-out $(platform_unavail), $^)
113113
touch $@
114114

115115
cprover_library.inc: library/converter$(EXEEXT) library/*.c

‎src/ansi-c/library/cprover_contracts.c

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -210,8 +210,8 @@ __CPROVER_HIDE:;
210210
CAR_SET_CONTAINS_LOOP:
211211
while(idx != 0)
212212
{
213-
incl |= candidate.is_writable & elem->is_writable &
214-
__CPROVER_same_object(elem->lb, candidate.lb) &
213+
incl |= (int)candidate.is_writable & (int)elem->is_writable &
214+
(int)__CPROVER_same_object(elem->lb, candidate.lb) &
215215
(__CPROVER_POINTER_OFFSET(elem->lb) <=
216216
__CPROVER_POINTER_OFFSET(candidate.lb)) &
217217
(__CPROVER_POINTER_OFFSET(candidate.ub) <=
@@ -798,7 +798,7 @@ __CPROVER_HIDE:;
798798
while(idx != 0)
799799
{
800800
incl |=
801-
elem->is_writable & __CPROVER_same_object(elem->lb, ptr) &
801+
(int)elem->is_writable & (int)__CPROVER_same_object(elem->lb, ptr) &
802802
(__CPROVER_POINTER_OFFSET(elem->lb) <= offset) &
803803
(__CPROVER_POINTER_OFFSET(ub) <= __CPROVER_POINTER_OFFSET(elem->ub));
804804
++elem;
@@ -1045,8 +1045,9 @@ __CPROVER_HIDE:;
10451045
// call free only iff the pointer is valid preconditions are met
10461046
// skip checks on r_ok, dynamic_object and pointer_offset
10471047
__CPROVER_bool preconditions =
1048-
(ptr == 0) | (__CPROVER_r_ok(ptr, 0) & __CPROVER_DYNAMIC_OBJECT(ptr) &
1049-
(__CPROVER_POINTER_OFFSET(ptr) == 0));
1048+
(ptr == 0) |
1049+
((int)__CPROVER_r_ok(ptr, 0) & (int)__CPROVER_DYNAMIC_OBJECT(ptr) &
1050+
(__CPROVER_POINTER_OFFSET(ptr) == 0));
10501051
// If there is aliasing between the pointers in the freeable set,
10511052
// and we attempt to free again one of the already freed pointers,
10521053
// the r_ok condition above will fail, preventing us to deallocate

‎src/ansi-c/library/stdio.c

Lines changed: 72 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -824,15 +824,17 @@ void perror(const char *s)
824824

825825
/* FUNCTION: fscanf */
826826

827-
#ifndef __CPROVER_STDIO_H_INCLUDED
828-
#include <stdio.h>
829-
#define __CPROVER_STDIO_H_INCLUDED
830-
#endif
827+
#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
831828

832-
#ifndef __CPROVER_STDARG_H_INCLUDED
833-
#include <stdarg.h>
834-
#define __CPROVER_STDARG_H_INCLUDED
835-
#endif
829+
# ifndef __CPROVER_STDIO_H_INCLUDED
830+
# include <stdio.h>
831+
# define __CPROVER_STDIO_H_INCLUDED
832+
# endif
833+
834+
# ifndef __CPROVER_STDARG_H_INCLUDED
835+
# include <stdarg.h>
836+
# define __CPROVER_STDARG_H_INCLUDED
837+
# endif
836838

837839
int fscanf(FILE *restrict stream, const char *restrict format, ...)
838840
{
@@ -844,6 +846,8 @@ __CPROVER_HIDE:;
844846
return result;
845847
}
846848

849+
#endif
850+
847851
/* FUNCTION: __isoc99_fscanf */
848852

849853
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -868,15 +872,17 @@ __CPROVER_HIDE:;
868872

869873
/* FUNCTION: scanf */
870874

871-
#ifndef __CPROVER_STDIO_H_INCLUDED
872-
#include <stdio.h>
873-
#define __CPROVER_STDIO_H_INCLUDED
874-
#endif
875+
#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
875876

876-
#ifndef __CPROVER_STDARG_H_INCLUDED
877-
#include <stdarg.h>
878-
#define __CPROVER_STDARG_H_INCLUDED
879-
#endif
877+
# ifndef __CPROVER_STDIO_H_INCLUDED
878+
# include <stdio.h>
879+
# define __CPROVER_STDIO_H_INCLUDED
880+
# endif
881+
882+
# ifndef __CPROVER_STDARG_H_INCLUDED
883+
# include <stdarg.h>
884+
# define __CPROVER_STDARG_H_INCLUDED
885+
# endif
880886

881887
int scanf(const char *restrict format, ...)
882888
{
@@ -888,6 +894,8 @@ __CPROVER_HIDE:;
888894
return result;
889895
}
890896

897+
#endif
898+
891899
/* FUNCTION: __isoc99_scanf */
892900

893901
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -912,15 +920,17 @@ __CPROVER_HIDE:;
912920

913921
/* FUNCTION: sscanf */
914922

915-
#ifndef __CPROVER_STDIO_H_INCLUDED
916-
#include <stdio.h>
917-
#define __CPROVER_STDIO_H_INCLUDED
918-
#endif
923+
#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
919924

920-
#ifndef __CPROVER_STDARG_H_INCLUDED
921-
#include <stdarg.h>
922-
#define __CPROVER_STDARG_H_INCLUDED
923-
#endif
925+
# ifndef __CPROVER_STDIO_H_INCLUDED
926+
# include <stdio.h>
927+
# define __CPROVER_STDIO_H_INCLUDED
928+
# endif
929+
930+
# ifndef __CPROVER_STDARG_H_INCLUDED
931+
# include <stdarg.h>
932+
# define __CPROVER_STDARG_H_INCLUDED
933+
# endif
924934

925935
int sscanf(const char *restrict s, const char *restrict format, ...)
926936
{
@@ -932,6 +942,8 @@ __CPROVER_HIDE:;
932942
return result;
933943
}
934944

945+
#endif
946+
935947
/* FUNCTION: __isoc99_sscanf */
936948

937949
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -956,15 +968,17 @@ __CPROVER_HIDE:;
956968

957969
/* FUNCTION: vfscanf */
958970

959-
#ifndef __CPROVER_STDIO_H_INCLUDED
960-
#include <stdio.h>
961-
#define __CPROVER_STDIO_H_INCLUDED
962-
#endif
971+
#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
963972

964-
#ifndef __CPROVER_STDARG_H_INCLUDED
965-
#include <stdarg.h>
966-
#define __CPROVER_STDARG_H_INCLUDED
967-
#endif
973+
# ifndef __CPROVER_STDIO_H_INCLUDED
974+
# include <stdio.h>
975+
# define __CPROVER_STDIO_H_INCLUDED
976+
# endif
977+
978+
# ifndef __CPROVER_STDARG_H_INCLUDED
979+
# include <stdarg.h>
980+
# define __CPROVER_STDARG_H_INCLUDED
981+
# endif
968982

969983
int __VERIFIER_nondet_int();
970984

@@ -998,6 +1012,8 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
9981012
return result;
9991013
}
10001014

1015+
#endif
1016+
10011017
/* FUNCTION: __isoc99_vfscanf */
10021018

10031019
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -1098,22 +1114,26 @@ int __stdio_common_vfscanf(
10981114

10991115
/* FUNCTION: vscanf */
11001116

1101-
#ifndef __CPROVER_STDIO_H_INCLUDED
1102-
#include <stdio.h>
1103-
#define __CPROVER_STDIO_H_INCLUDED
1104-
#endif
1117+
#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
11051118

1106-
#ifndef __CPROVER_STDARG_H_INCLUDED
1107-
#include <stdarg.h>
1108-
#define __CPROVER_STDARG_H_INCLUDED
1109-
#endif
1119+
# ifndef __CPROVER_STDIO_H_INCLUDED
1120+
# include <stdio.h>
1121+
# define __CPROVER_STDIO_H_INCLUDED
1122+
# endif
1123+
1124+
# ifndef __CPROVER_STDARG_H_INCLUDED
1125+
# include <stdarg.h>
1126+
# define __CPROVER_STDARG_H_INCLUDED
1127+
# endif
11101128

11111129
int vscanf(const char *restrict format, va_list arg)
11121130
{
11131131
__CPROVER_HIDE:;
11141132
return vfscanf(stdin, format, arg);
11151133
}
11161134

1135+
#endif
1136+
11171137
/* FUNCTION: __isoc99_vscanf */
11181138

11191139
#ifndef __CPROVER_STDIO_H_INCLUDED
@@ -1134,15 +1154,17 @@ __CPROVER_HIDE:;
11341154

11351155
/* FUNCTION: vsscanf */
11361156

1137-
#ifndef __CPROVER_STDIO_H_INCLUDED
1138-
#include <stdio.h>
1139-
#define __CPROVER_STDIO_H_INCLUDED
1140-
#endif
1157+
#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
11411158

1142-
#ifndef __CPROVER_STDARG_H_INCLUDED
1143-
#include <stdarg.h>
1144-
#define __CPROVER_STDARG_H_INCLUDED
1145-
#endif
1159+
# ifndef __CPROVER_STDIO_H_INCLUDED
1160+
# include <stdio.h>
1161+
# define __CPROVER_STDIO_H_INCLUDED
1162+
# endif
1163+
1164+
# ifndef __CPROVER_STDARG_H_INCLUDED
1165+
# include <stdarg.h>
1166+
# define __CPROVER_STDARG_H_INCLUDED
1167+
# endif
11461168

11471169
int __VERIFIER_nondet_int();
11481170

@@ -1162,6 +1184,8 @@ __CPROVER_HIDE:;
11621184
return result;
11631185
}
11641186

1187+
#endif
1188+
11651189
/* FUNCTION: __isoc99_vsscanf */
11661190

11671191
#ifndef __CPROVER_STDIO_H_INCLUDED

‎src/ansi-c/library_check.sh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ for f in "$@"; do
1212
perl -p -i -e 's/(_mm_.fence)/s$1/' __libcheck.c
1313
perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
1414
perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c
15-
"$CC" -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
16-
"$CC" -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
15+
$CC -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
16+
$CC -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
1717
-o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas
1818
ec="${?}"
1919
rm __libcheck.s __libcheck.i __libcheck.c

‎src/cpp/CMakeLists.txt

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,13 +24,24 @@ endif()
2424

2525
################################################################################
2626

27+
set(extra_dependencies
28+
${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
29+
${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
30+
)
31+
32+
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
33+
list(REMOVE_ITEM
34+
extra_dependencies
35+
${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp)
36+
endif()
37+
2738
file(GLOB_RECURSE sources "*.cpp" "*.h")
2839
add_library(cpp ${sources})
2940

3041
set_source_files_properties(
3142
${sources}
3243
PROPERTIES
33-
OBJECT_DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
44+
OBJECT_DEPENDS "${extra_dependencies}"
3445
)
3546

3647
generic_includes(cpp)

‎src/cpp/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ cprover_library$(OBJEXT): cprover_library.inc
6969
$(MAKE) -C ../ansi-c library/converter$(EXEEXT)
7070

7171
library_check: library/*.c
72-
../ansi-c/library_check.sh $(CC) $^
72+
../ansi-c/library_check.sh "$(CC)" $^
7373
touch $@
7474

7575
cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c

0 commit comments

Comments
 (0)