From 58accc33772e3f61261f622a6d07eed7d67576fe Mon Sep 17 00:00:00 2001 From: Shuhao Zhang Date: Sat, 30 May 2026 01:44:27 +0800 Subject: [PATCH 1/7] util/unit: avoid GCC 16 array-bounds warnings in json string ranges GCC 16 reports false-positive -Warray-bounds warnings through the ranget::map shared_ptr/std::function instantiations used with json_stringt values. Build the source-location pragma JSON array explicitly, and keep json_arrayt range-construction coverage by collecting an existing range of json_stringt values directly. This avoids the warning path without changing the JSON output or tested behaviour. --- src/util/json_irep.cpp | 9 ++++----- unit/util/json_array.cpp | 15 +++++---------- unit/util/json_object.cpp | 29 +++++++++++++++++++++++++++++ 3 files changed, 38 insertions(+), 15 deletions(-) diff --git a/src/util/json_irep.cpp b/src/util/json_irep.cpp index 2fc56264a7b..8600e1d99ff 100644 --- a/src/util/json_irep.cpp +++ b/src/util/json_irep.cpp @@ -185,11 +185,10 @@ json_objectt json(const source_locationt &location) const auto &pragmas = location.get_pragmas(); if(!pragmas.empty()) { - auto json_pragma_range = make_range(pragmas.begin(), pragmas.end()) - .map([](const std::pair &entry) - { return json_stringt{entry.first}; }); - result["pragma"] = - json_arrayt{json_pragma_range.begin(), json_pragma_range.end()}; + json_arrayt json_pragmas; + for(const auto &pragma : pragmas) + json_pragmas.push_back(json_stringt{pragma.first}); + result["pragma"] = std::move(json_pragmas); } return result; diff --git a/unit/util/json_array.cpp b/unit/util/json_array.cpp index 1c233ee25d2..382275a22ff 100644 --- a/unit/util/json_array.cpp +++ b/unit/util/json_array.cpp @@ -7,11 +7,9 @@ Author: Diffblue Ltd. \*******************************************************************/ #include -#include #include #include -#include #include SCENARIO( @@ -43,16 +41,13 @@ SCENARIO( "Test that json_arrayt can be constructed using `ranget`", "[core][util][json]") { - GIVEN("A vector of strings.") + GIVEN("A vector of json strings.") { - const std::vector input{"foo", "bar"}; - THEN( - "A json_arrayt can be constructed from the vector of strings using range " - "and map.") + const std::vector input{ + json_stringt{"foo"}, json_stringt{"bar"}}; + THEN("A json_arrayt can be constructed from the vector using range.") { - const json_arrayt array = make_range(input) - .map(constructor_of()) - .collect(); + const json_arrayt array = make_range(input).collect(); auto it = array.begin(); REQUIRE(it->kind == jsont::kindt::J_STRING); REQUIRE(it->value == "foo"); diff --git a/unit/util/json_object.cpp b/unit/util/json_object.cpp index 74d70147fb3..94f1f282558 100644 --- a/unit/util/json_object.cpp +++ b/unit/util/json_object.cpp @@ -9,8 +9,10 @@ Author: Diffblue Ltd. #include #include +#include #include #include +#include #include #include @@ -104,3 +106,30 @@ SCENARIO( }; } } + +SCENARIO( + "Test that source location pragmas are converted to JSON arrays.", + "[core][util][json]") +{ + GIVEN("A source location with pragmas.") + { + source_locationt location; + location.add_pragma("disable:pointer-check"); + location.add_pragma("disable:bounds-check"); + + THEN("The pragmas are emitted as strings.") + { + const json_objectt output = json(location); + const json_arrayt &pragmas = to_json_array(output["pragma"]); + + auto pragma_it = pragmas.begin(); + REQUIRE(pragma_it->kind == jsont::kindt::J_STRING); + REQUIRE(pragma_it->value == "disable:bounds-check"); + ++pragma_it; + REQUIRE(pragma_it->kind == jsont::kindt::J_STRING); + REQUIRE(pragma_it->value == "disable:pointer-check"); + ++pragma_it; + REQUIRE(pragma_it == pragmas.end()); + } + } +} From b43cd4c497e54d19e0e2fab4c8e340ed7c0c939b Mon Sep 17 00:00:00 2001 From: Shuhao Zhang Date: Sat, 30 May 2026 01:44:51 +0800 Subject: [PATCH 2/7] variable-sensitivity: avoid GCC 16 array-bounds warnings from virtual dispatch GCC 16 can report false-positive -Warray-bounds warnings after devirtualising and inlining calls on base-class objects as if derived-class layouts were available. Call the known base implementations explicitly in the variable-sensitivity factory and the corresponding unit-test helper. The constructed dynamic types are unchanged, and the explicit calls avoid the over-eager diagnostic path. --- .../variable-sensitivity/variable_sensitivity_domain.h | 2 +- unit/analyses/variable-sensitivity/eval-member-access.cpp | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index 707de155078..b89ce29483b 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -266,7 +266,7 @@ class variable_sensitivity_domain_factoryt { auto d = std::make_unique( object_factory, configuration); - CHECK_RETURN(d->is_bottom()); + CHECK_RETURN(d->variable_sensitivity_domaint::is_bottom()); return std::unique_ptr(d.release()); } diff --git a/unit/analyses/variable-sensitivity/eval-member-access.cpp b/unit/analyses/variable-sensitivity/eval-member-access.cpp index dceb954181b..3471f0f1cbc 100644 --- a/unit/analyses/variable-sensitivity/eval-member-access.cpp +++ b/unit/analyses/variable-sensitivity/eval-member-access.cpp @@ -161,7 +161,6 @@ exprt integer_expression(int i) exprt top_expression() { - auto top_value = - std::make_shared(integer_typet(), true, false); - return top_value->to_constant(); + abstract_objectt top_value(integer_typet(), true, false); + return top_value.abstract_objectt::to_constant(); } From 9d9f6f47d2979caf78c92664cfdf105aee5bfbf1 Mon Sep 17 00:00:00 2001 From: Shuhao Zhang Date: Sat, 30 May 2026 01:45:10 +0800 Subject: [PATCH 3/7] smt2 incremental: avoid reference_wrapper on incomplete namespace type GCC 16 warns when std::reference_wrapper is instantiated while namespacet is still incomplete in struct_encoding.h. Use a plain reference member instead. struct_encodingt already binds to an external namespace for its lifetime, so this preserves behaviour while avoiding -Wsfinae-incomplete under -Werror. --- src/solvers/smt2_incremental/encoding/struct_encoding.cpp | 7 +++---- src/solvers/smt2_incremental/encoding/struct_encoding.h | 2 +- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp index baf18f3187d..2444fc10f11 100644 --- a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -176,8 +176,7 @@ exprt struct_encodingt::encode_member(const member_exprt &member_expr) const } const auto &struct_type = compound_type.id() == ID_struct_tag - ? ns.get().follow_tag( - type_checked_cast(compound_type)) + ? ns.follow_tag(type_checked_cast(compound_type)) : type_checked_cast(compound_type); return count_trailing_bit_width( struct_type, member_expr.get_component_name(), *boolbv_width); @@ -243,7 +242,7 @@ exprt struct_encodingt::decode( INVARIANT( can_cast_type(encoded.type()), "Structs are expected to be encoded into bit vectors."); - const struct_typet definition = ns.get().follow_tag(original_type); + const struct_typet definition = ns.follow_tag(original_type); exprt::operandst encoded_fields; for(const auto &component : definition.components()) { @@ -261,7 +260,7 @@ exprt struct_encodingt::decode( INVARIANT( can_cast_type(encoded.type()), "Unions are expected to be encoded into bit vectors."); - const union_typet definition = ns.get().follow_tag(original_type); + const union_typet definition = ns.follow_tag(original_type); const auto &components = definition.components(); if(components.empty()) return empty_union_exprt{original_type}; diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.h b/src/solvers/smt2_incremental/encoding/struct_encoding.h index bb19a0110c4..0c499f79106 100644 --- a/src/solvers/smt2_incremental/encoding/struct_encoding.h +++ b/src/solvers/smt2_incremental/encoding/struct_encoding.h @@ -33,7 +33,7 @@ class struct_encodingt final private: std::unique_ptr boolbv_width; - std::reference_wrapper ns; + const namespacet &ns; exprt encode_member(const member_exprt &member_expr) const; }; From 3c4285efd756b21bc4b5aa57e4bcef38b077d3d2 Mon Sep 17 00:00:00 2001 From: Shuhao Zhang Date: Sat, 30 May 2026 01:45:23 +0800 Subject: [PATCH 4/7] smt2: remove unused struct component counter The counter in smt2_convt::unflatten was incremented while converting datatype structs but was never read. Remove it, and keep the touched loop formatted, to avoid the GCC 16 -Wunused-but-set-variable warning under -Werror without changing the generated SMT2 output. --- src/solvers/smt2/smt2_conv.cpp | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 8dada3f3e24..8f48de19c69 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -5378,11 +5378,9 @@ void smt2_convt::unflatten( std::size_t offset=0; - std::size_t i=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++, i++) + for(struct_typet::componentst::const_iterator it = components.begin(); + it != components.end(); + it++) { if(is_zero_width(it->type(), ns)) continue; From 4bcebdccf0c50ff67019e4e19913b129a1662f42 Mon Sep 17 00:00:00 2001 From: Shuhao Zhang Date: Tue, 2 Jun 2026 00:01:44 +0800 Subject: [PATCH 5/7] unit: avoid assuming source-location pragma order The source-location pragma JSON test should check the emitted pragma set rather than the iteration order of irept::named_subt. Collect and sort the JSON string values before comparing them so the test remains stable across named_subt implementations and dstring interning order. --- unit/util/json_object.cpp | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/unit/util/json_object.cpp b/unit/util/json_object.cpp index 94f1f282558..e62cc54b933 100644 --- a/unit/util/json_object.cpp +++ b/unit/util/json_object.cpp @@ -122,14 +122,18 @@ SCENARIO( const json_objectt output = json(location); const json_arrayt &pragmas = to_json_array(output["pragma"]); - auto pragma_it = pragmas.begin(); - REQUIRE(pragma_it->kind == jsont::kindt::J_STRING); - REQUIRE(pragma_it->value == "disable:bounds-check"); - ++pragma_it; - REQUIRE(pragma_it->kind == jsont::kindt::J_STRING); - REQUIRE(pragma_it->value == "disable:pointer-check"); - ++pragma_it; - REQUIRE(pragma_it == pragmas.end()); + std::vector pragma_values; + for(const auto &pragma : pragmas) + { + REQUIRE(pragma.kind == jsont::kindt::J_STRING); + pragma_values.push_back(pragma.value); + } + + std::sort(pragma_values.begin(), pragma_values.end()); + REQUIRE( + pragma_values == + std::vector{ + "disable:bounds-check", "disable:pointer-check"}); } } } From 6a3f2c291780cb6ecbffc8d0659520d052229516 Mon Sep 17 00:00:00 2001 From: Shuhao Zhang Date: Tue, 2 Jun 2026 00:12:42 +0800 Subject: [PATCH 6/7] unit: format JSON test includes Move the testing-utils include after util includes in the JSON unit tests to match clang-format-15 include ordering. --- unit/util/json_array.cpp | 3 ++- unit/util/json_object.cpp | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/unit/util/json_array.cpp b/unit/util/json_array.cpp index 382275a22ff..193e10f54f2 100644 --- a/unit/util/json_array.cpp +++ b/unit/util/json_array.cpp @@ -6,10 +6,11 @@ Author: Diffblue Ltd. \*******************************************************************/ -#include #include #include +#include + #include SCENARIO( diff --git a/unit/util/json_object.cpp b/unit/util/json_object.cpp index e62cc54b933..77399b8d555 100644 --- a/unit/util/json_object.cpp +++ b/unit/util/json_object.cpp @@ -6,14 +6,14 @@ Author: Diffblue Ltd. \*******************************************************************/ -#include - #include #include #include #include #include +#include + #include #include #include From 83f4ae87a49389d0a70e53689f09725abd63a532 Mon Sep 17 00:00:00 2001 From: Shuhao Zhang Date: Fri, 2 Oct 2026 03:29:36 +0800 Subject: [PATCH 7/7] unit/util: format --- unit/util/json_object.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/unit/util/json_object.cpp b/unit/util/json_object.cpp index 77399b8d555..2771c3f2975 100644 --- a/unit/util/json_object.cpp +++ b/unit/util/json_object.cpp @@ -131,9 +131,8 @@ SCENARIO( std::sort(pragma_values.begin(), pragma_values.end()); REQUIRE( - pragma_values == - std::vector{ - "disable:bounds-check", "disable:pointer-check"}); + pragma_values == std::vector{ + "disable:bounds-check", "disable:pointer-check"}); } } }