Skip to content

Commit 560a588

Browse files
tautschnigtautschnig
committed
Add support for building with GCC 14
GCC 14 adds new warnings. Those are largely spurious (perhaps with exception of the interpreter code and unit tests), but still require working around. These warnings also affect CaDiCaL builds, which in turn requires us to upgrade to version 2.0.0, where workarounds have been added. Fixes: #7749
1 parent 66ae03f commit 560a588

File tree

23 files changed

+124
-74
lines changed

23 files changed

+124
-74
lines changed

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -399,7 +399,7 @@ jobs:
399399
run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
400400

401401
# This job takes approximately 14 to 46 minutes
402-
check-ubuntu-24_04-cmake-gcc-13:
402+
check-ubuntu-24_04-cmake-gcc-14:
403403
runs-on: ubuntu-24.04
404404
steps:
405405
- uses: actions/checkout@v4
@@ -412,13 +412,13 @@ jobs:
412412
DEBIAN_FRONTEND: noninteractive
413413
run: |
414414
sudo apt-get update
415-
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-13 gdb g++-13 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
415+
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-14 gdb g++-14 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
416416
# Update symlinks so that any use of gcc (including our regression
417-
# tests) will use GCC 13.
418-
sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-13 110 \
419-
--slave /usr/bin/g++ g++ /usr/bin/g++-13 \
420-
--slave /usr/bin/gcov gcov /usr/bin/gcov-13
421-
sudo ln -sf cpp-13 /usr/bin/cpp
417+
# tests) will use GCC 14.
418+
sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-14 110 \
419+
--slave /usr/bin/g++ g++ /usr/bin/g++-14 \
420+
--slave /usr/bin/gcov gcov /usr/bin/gcov-14
421+
sudo ln -sf cpp-14 /usr/bin/cpp
422422
- name: Confirm z3 solver is available and log the version installed
423423
run: z3 --version
424424
- name: Download cvc-5 from the releases page and make sure it can be deployed
@@ -432,10 +432,10 @@ jobs:
432432
with:
433433
save-always: true
434434
path: .ccache
435-
key: ${{ runner.os }}-24.04-Release-gcc-13-${{ github.ref }}-${{ github.sha }}-PR
435+
key: ${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }}-${{ github.sha }}-PR
436436
restore-keys: |
437-
${{ runner.os }}-24.04-Release-gcc-13-${{ github.ref }}
438-
${{ runner.os }}-24.04-Release-gcc-13
437+
${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }}
438+
${{ runner.os }}-24.04-Release-gcc-14
439439
- name: ccache environment
440440
run: |
441441
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV

‎jbmc/src/java_bytecode/assignments_from_json.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -641,8 +641,9 @@ static code_with_references_listt assign_enum_from_json(
641641

642642
dereference_exprt values_struct{
643643
info.symbol_table.lookup_ref(values_name).symbol_expr()};
644-
const auto &values_struct_type = namespacet{info.symbol_table}.follow_tag(
645-
to_struct_tag_type(values_struct.type()));
644+
const namespacet ns{info.symbol_table};
645+
const auto &values_struct_type =
646+
ns.follow_tag(to_struct_tag_type(values_struct.type()));
646647
PRECONDITION(is_valid_java_array(values_struct_type));
647648
const member_exprt values_data = member_exprt{
648649
values_struct, "data", values_struct_type.components()[2].type()};

‎jbmc/src/java_bytecode/java_utils.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -164,7 +164,11 @@ bool is_non_null_library_global(const irep_idt &);
164164

165165
extern const std::unordered_set<std::string> cprover_methods_to_ignore;
166166

167-
symbolt &fresh_java_symbol(
167+
#if defined(__GNUC__) && __GNUC__ >= 14
168+
[[gnu::no_dangling]]
169+
#endif
170+
symbolt &
171+
fresh_java_symbol(
168172
const typet &type,
169173
const std::string &basename_prefix,
170174
const source_locationt &source_location,

‎jbmc/src/java_bytecode/lambda_synthesis.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -444,7 +444,11 @@ void create_invokedynamic_synthetic_classes(
444444
}
445445
}
446446

447-
static const symbolt &get_or_create_method_symbol(
447+
#if defined(__GNUC__) && __GNUC__ >= 14
448+
[[gnu::no_dangling]]
449+
#endif
450+
static const symbolt &
451+
get_or_create_method_symbol(
448452
const irep_idt &identifier,
449453
const irep_idt &base_name,
450454
const irep_idt &pretty_name,

‎jbmc/unit/java-testing-utils/require_goto_statements.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -381,7 +381,7 @@ get_ultimate_source_symbol(
381381
/// \return The identifier of the ultimate source symbol assigned to the field,
382382
/// which will be used for future calls to
383383
/// `require_struct_component_assignment`.
384-
const irep_idt &require_goto_statements::require_struct_component_assignment(
384+
irep_idt require_goto_statements::require_struct_component_assignment(
385385
const irep_idt &structure_name,
386386
const std::optional<irep_idt> &superclass_name,
387387
const irep_idt &component_name,
@@ -514,8 +514,7 @@ require_goto_statements::require_struct_array_component_assignment(
514514
/// \param argument_name: Name of the input argument of method under test
515515
/// \param entry_point_statements: The statements to look through
516516
/// \return The identifier of the variable assigned to the input argument
517-
const irep_idt &
518-
require_goto_statements::require_entry_point_argument_assignment(
517+
irep_idt require_goto_statements::require_entry_point_argument_assignment(
519518
const irep_idt &argument_name,
520519
const std::vector<codet> &entry_point_statements)
521520
{

‎jbmc/unit/java-testing-utils/require_goto_statements.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ const code_declt &require_declaration_of_name(
7272
const irep_idt &variable_name,
7373
const std::vector<codet> &entry_point_instructions);
7474

75-
const irep_idt &require_struct_component_assignment(
75+
irep_idt require_struct_component_assignment(
7676
const irep_idt &structure_name,
7777
const std::optional<irep_idt> &superclass_name,
7878
const irep_idt &component_name,
@@ -89,7 +89,7 @@ const irep_idt &require_struct_array_component_assignment(
8989
const std::vector<codet> &entry_point_instructions,
9090
const symbol_table_baset &symbol_table);
9191

92-
const irep_idt &require_entry_point_argument_assignment(
92+
irep_idt require_entry_point_argument_assignment(
9393
const irep_idt &argument_name,
9494
const std::vector<codet> &entry_point_statements);
9595

‎jbmc/unit/java-testing-utils/require_type.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,9 @@ namespace require_type
2424
pointer_typet
2525
require_pointer(const typet &type, const std::optional<typet> &subtype);
2626

27+
#if defined(__GNUC__) && __GNUC__ >= 14
28+
[[gnu::no_dangling]]
29+
#endif
2730
const struct_tag_typet &
2831
require_struct_tag(const typet &type, const irep_idt &identifier = "");
2932

‎scripts/cadical-1.7.2-patch renamed to ‎scripts/cadical-2.0.0-patch

File renamed without changes.

‎scripts/cadical_CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ add_library(cadical ${sources})
99

1010
# Pass -DNBUILD to disable including the version information, which is not
1111
# needed since cbmc doesn't run the cadical binary
12-
target_compile_options(cadical PUBLIC -DNBUILD)
12+
target_compile_options(cadical PUBLIC -DNBUILD -DNFLEXIBLE)
1313

1414
set_target_properties(
1515
cadical

‎src/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -186,14 +186,14 @@ glucose-download:
186186
@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
187187
@$(RM) $(glucose_rev).tar.gz
188188

189-
cadical_release = rel-1.7.2
189+
cadical_release = rel-2.0.0
190190
cadical-download:
191191
@echo "Downloading CaDiCaL $(cadical_release)"
192192
@$(DOWNLOADER) https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz
193193
@$(TAR) xfz $(cadical_release).tar.gz
194194
@rm -Rf ../cadical
195195
@mv cadical-$(cadical_release) ../cadical
196-
@(cd ../cadical; patch -p1 < ../scripts/cadical-1.7.2-patch)
196+
@(cd ../cadical; patch -p1 < ../scripts/cadical-2.0.0-patch)
197197
@(cd ../cadical && ./configure CXX="$(CXX)")
198198
# Need to rename VERSION so that it isn't picked up by `#include<version>` on
199199
# macOS which is case insensitive

‎src/ansi-c/compiler_headers/gcc_builtin_headers_types.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,12 @@ typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16)));
3232
typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32)));
3333
typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64)));
3434
typedef unsigned short __gcc_v32uhi __attribute__ ((__vector_size__ (64)));
35+
typedef unsigned int __gcc_v4usi __attribute__ ((__vector_size__ (16)));
36+
typedef unsigned int __gcc_v8usi __attribute__ ((__vector_size__ (32)));
3537
typedef unsigned int __gcc_v16usi __attribute__ ((__vector_size__ (64)));
3638
typedef unsigned long long __gcc_di;
39+
typedef unsigned long long __gcc_v2udi __attribute__ ((__vector_size__ (16)));
40+
typedef unsigned long long __gcc_v4udi __attribute__ ((__vector_size__ (32)));
3741
typedef unsigned long long __gcc_v8udi __attribute__ ((__vector_size__ (64)));
3842

3943
enum __gcc_atomic_memmodels {

‎src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,11 @@ struct dfcc_utilst
7272
const bool no_nondet_initialization = true);
7373

7474
/// Creates a new parameter symbol for the given function_id
75-
static const symbolt &create_new_parameter_symbol(
75+
#if defined(__GNUC__) && __GNUC__ >= 14
76+
[[gnu::no_dangling]]
77+
#endif
78+
static const symbolt &
79+
create_new_parameter_symbol(
7680
symbol_table_baset &,
7781
const irep_idt &function_id,
7882
const std::string &base_name,
@@ -100,7 +104,11 @@ struct dfcc_utilst
100104
/// The cloned function symbol has `new_function_id` as name
101105
/// The cloned parameters symbols have `new_function_id::name` as name
102106
/// Returns the new function symbol
103-
static const symbolt &clone_and_rename_function(
107+
#if defined(__GNUC__) && __GNUC__ >= 14
108+
[[gnu::no_dangling]]
109+
#endif
110+
static const symbolt &
111+
clone_and_rename_function(
104112
goto_modelt &goto_model,
105113
const irep_idt &function_id,
106114
const irep_idt &new_function_id,

‎src/goto-programs/interpreter.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -607,7 +607,7 @@ exprt interpretert::get_value(
607607
{
608608
// We want the symbol pointed to
609609
mp_integer address = rhs[numeric_cast_v<std::size_t>(offset)];
610-
const symbol_exprt &symbol_expr = address_to_symbol(address);
610+
const symbol_exprt symbol_expr = address_to_symbol(address);
611611
mp_integer offset_from_address = address_to_offset(address);
612612

613613
if(offset_from_address == 0)
@@ -751,7 +751,7 @@ void interpretert::execute_function_call()
751751
#if 0
752752
const memory_cellt &cell=memory[address];
753753
#endif
754-
const irep_idt &identifier = address_to_symbol(address).get_identifier();
754+
const irep_idt identifier = address_to_symbol(address).get_identifier();
755755
trace_step.called_function = identifier;
756756

757757
const goto_functionst::function_mapt::const_iterator f_it=

‎src/goto-programs/mm_io.cpp

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -54,15 +54,14 @@ mm_iot::mm_iot(symbol_table_baset &symbol_table)
5454
{
5555
mm_io_r = mm_io_r_symbol->symbol_expr();
5656

57-
const auto &value_symbol = get_fresh_aux_symbol(
58-
to_code_type(mm_io_r.type()).return_type(),
59-
id2string(id_r) + "$value",
60-
id2string(id_r) + "$value",
61-
mm_io_r_symbol->location,
62-
mm_io_r_symbol->mode,
63-
symbol_table);
64-
65-
mm_io_r_value = value_symbol.symbol_expr();
57+
mm_io_r_value = get_fresh_aux_symbol(
58+
to_code_type(mm_io_r.type()).return_type(),
59+
id2string(id_r) + "$value",
60+
id2string(id_r) + "$value",
61+
mm_io_r_symbol->location,
62+
mm_io_r_symbol->mode,
63+
symbol_table)
64+
.symbol_expr();
6665
}
6766

6867
if(const auto mm_io_w_symbol = symbol_table.lookup(id_w))

‎src/goto-symex/goto_symex.cpp

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -347,16 +347,18 @@ void goto_symext::associate_array_to_pointer(
347347
const function_application_exprt array_to_pointer_app{
348348
function_symbol.symbol_expr(), {new_char_array, string_data}};
349349

350-
const symbolt &return_symbol = get_fresh_aux_symbol(
351-
to_mathematical_function_type(function_symbol.type).codomain(),
352-
"",
353-
"return_value",
354-
source_locationt(),
355-
function_symbol.mode,
356-
ns,
357-
state.symbol_table);
358-
359-
const ssa_exprt ssa_expr(return_symbol.symbol_expr());
350+
symbol_exprt return_symbol_expr =
351+
get_fresh_aux_symbol(
352+
to_mathematical_function_type(function_symbol.type).codomain(),
353+
"",
354+
"return_value",
355+
source_locationt(),
356+
function_symbol.mode,
357+
ns,
358+
state.symbol_table)
359+
.symbol_expr();
360+
361+
const ssa_exprt ssa_expr(return_symbol_expr);
360362

361363
symex_assign.assign_symbol(
362364
ssa_expr, expr_skeletont{}, array_to_pointer_app, {});

‎src/goto-symex/shadow_memory.cpp

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -71,17 +71,19 @@ const symbol_exprt &shadow_memoryt::add_field(
7171
const typet &field_type)
7272
{
7373
const auto &function_symbol = ns.lookup(state.source.function_id);
74-
const symbolt &new_symbol = get_fresh_aux_symbol(
75-
field_type,
76-
id2string(state.source.function_id),
77-
SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name),
78-
state.source.pc->source_location(),
79-
function_symbol.mode,
80-
state.symbol_table);
74+
symbol_exprt new_symbol_expr =
75+
get_fresh_aux_symbol(
76+
field_type,
77+
id2string(state.source.function_id),
78+
SHADOW_MEMORY_PREFIX + from_expr(expr) + "__" + id2string(field_name),
79+
state.source.pc->source_location(),
80+
function_symbol.mode,
81+
state.symbol_table)
82+
.symbol_expr();
8183

8284
auto &addresses = state.shadow_memory.address_fields[field_name];
8385
addresses.push_back(
84-
shadow_memory_statet::shadowed_addresst{expr, new_symbol.symbol_expr()});
86+
shadow_memory_statet::shadowed_addresst{expr, new_symbol_expr});
8587

8688
return addresses.back().shadow;
8789
}

‎src/goto-symex/symex_dereference.cpp

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -215,14 +215,15 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
215215
return *cached;
216216
}
217217

218-
auto const &cache_symbol = get_fresh_aux_symbol(
219-
cache_key.type(),
220-
"symex",
221-
"dereference_cache",
222-
dereference_result.source_location(),
223-
language_mode,
224-
ns,
225-
state.symbol_table);
218+
auto cache_symbol_expr = get_fresh_aux_symbol(
219+
cache_key.type(),
220+
"symex",
221+
"dereference_cache",
222+
dereference_result.source_location(),
223+
language_mode,
224+
ns,
225+
state.symbol_table)
226+
.symbol_expr();
226227

227228
// we need to lift possible lets
228229
// (come from the value set to avoid repeating complex pointer comparisons)
@@ -237,7 +238,6 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
237238
symex_config,
238239
target};
239240

240-
auto cache_symbol_expr = cache_symbol.symbol_expr();
241241
assign.assign_symbol(
242242
to_ssa_expr(state.rename<L1>(cache_symbol_expr, ns).get()),
243243
expr_skeletont{},

‎src/solvers/CMakeLists.txt

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -121,11 +121,11 @@ foreach(SOLVER ${sat_impl})
121121
message(STATUS "Building solvers with cadical")
122122

123123
download_project(PROJ cadical
124-
URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz
125-
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch
124+
URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
125+
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch
126126
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt
127127
COMMAND ./configure
128-
URL_MD5 be646831a017f81b300664e58deba1b5
128+
URL_MD5 9fc2a66196b86adceb822a583318cc35
129129
)
130130

131131
add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
@@ -144,10 +144,10 @@ foreach(SOLVER ${sat_impl})
144144
message(STATUS "Building with IPASIR solver linking against: CaDiCaL")
145145

146146
download_project(PROJ cadical
147-
URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz
148-
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch
147+
URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
148+
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch
149149
COMMAND ./configure
150-
URL_MD5 be646831a017f81b300664e58deba1b5
150+
URL_MD5 9fc2a66196b86adceb822a583318cc35
151151
)
152152

153153
message(STATUS "Building CaDiCaL")

‎src/solvers/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -281,7 +281,7 @@ solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB)
281281
$(LINKLIB)
282282

283283
../../cadical/build/libcadical$(LIBEXT):
284-
$(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS)"
284+
$(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS) -DNFLEXIBLE"
285285

286286
-include smt2/smt2_solver$(DEPEXT)
287287

‎src/util/fresh_symbol.h

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,15 +22,23 @@ class symbolt;
2222
class symbol_table_baset;
2323
class typet;
2424

25-
symbolt &get_fresh_aux_symbol(
25+
#if defined(__GNUC__) && __GNUC__ >= 14
26+
[[gnu::no_dangling]]
27+
#endif
28+
symbolt &
29+
get_fresh_aux_symbol(
2630
const typet &type,
2731
const std::string &name_prefix,
2832
const std::string &basename_prefix,
2933
const source_locationt &source_location,
3034
const irep_idt &symbol_mode,
3135
symbol_table_baset &symbol_table);
3236

33-
symbolt &get_fresh_aux_symbol(
37+
#if defined(__GNUC__) && __GNUC__ >= 14
38+
[[gnu::no_dangling]]
39+
#endif
40+
symbolt &
41+
get_fresh_aux_symbol(
3442
const typet &type,
3543
const std::string &name_prefix,
3644
const std::string &basename_prefix,

0 commit comments

Comments
 (0)