From 55edd883f7e0604ff4ea158535d4b9a9abc92e91 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 30 Apr 2026 21:08:05 +0000 Subject: [PATCH 1/6] unit/miniBDD: Fix module dependencies The test uses boolbvt. --- unit/solvers/bdd/miniBDD/module_dependencies.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/unit/solvers/bdd/miniBDD/module_dependencies.txt b/unit/solvers/bdd/miniBDD/module_dependencies.txt index 08156c972ba..21f20fa7016 100644 --- a/unit/solvers/bdd/miniBDD/module_dependencies.txt +++ b/unit/solvers/bdd/miniBDD/module_dependencies.txt @@ -1,4 +1,5 @@ solvers/bdd/miniBDD +solvers/flattening solvers/prop testing-utils util From b33e65993358513553ea1c9a21952c20b322c350 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 30 Apr 2026 10:34:38 +0000 Subject: [PATCH 2/6] Add empty_namespacet for unit tests Introduce empty_namespacet, a namespacet subclass that self-contains an empty symbol_tablet member. This avoids the boilerplate of declaring a symbol_tablet and namespacet in every test that doesn't actually populate the symbol table. Follows the same pattern as the existing null_message_handler in testing-utils. Co-authored-by: Kiro --- unit/testing-utils/Makefile | 1 + unit/testing-utils/empty_namespace.cpp | 14 ++++++++++ unit/testing-utils/empty_namespace.h | 37 ++++++++++++++++++++++++++ 3 files changed, 52 insertions(+) create mode 100644 unit/testing-utils/empty_namespace.cpp create mode 100644 unit/testing-utils/empty_namespace.h diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index abe4cc78c22..893b15f0a1f 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -1,5 +1,6 @@ SRC = \ call_graph_test_utils.cpp \ + empty_namespace.cpp \ free_form_cmdline.cpp \ get_goto_model_from_c.cpp \ invariant.cpp \ diff --git a/unit/testing-utils/empty_namespace.cpp b/unit/testing-utils/empty_namespace.cpp new file mode 100644 index 00000000000..0513ef483f9 --- /dev/null +++ b/unit/testing-utils/empty_namespace.cpp @@ -0,0 +1,14 @@ +/*******************************************************************\ + +Module: Unit test utilities + +Author: Diffblue Limited. + +\*******************************************************************/ + +/// \file +/// Global instance of \ref empty_namespacet. + +#include "empty_namespacet.h" + +const empty_namespacet empty_namespace; diff --git a/unit/testing-utils/empty_namespace.h b/unit/testing-utils/empty_namespace.h new file mode 100644 index 00000000000..b06438701ab --- /dev/null +++ b/unit/testing-utils/empty_namespace.h @@ -0,0 +1,37 @@ +/*******************************************************************\ + +Module: Unit test utilities + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// An empty namespacet for unit tests that don't need symbols. + +#ifndef CPROVER_TESTING_UTILS_EMPTY_NAMESPACE_H +#define CPROVER_TESTING_UTILS_EMPTY_NAMESPACE_H + +#include +#include + +/// A namespacet that contains an empty symbol table, for use in tests that +/// need a namespacet but don't actually look up any symbols. +/// This avoids the boilerplate of declaring a symbol_tablet and namespacet +/// in every test. +class empty_namespacet : private symbol_tablet, public namespacet +{ +public: + empty_namespacet() : namespacet{*static_cast(this)} + { + } + + empty_namespacet(const empty_namespacet &) = delete; + empty_namespacet(empty_namespacet &&) = delete; + empty_namespacet &operator=(const empty_namespacet &) = delete; + empty_namespacet &operator=(empty_namespacet &&) = delete; +}; + +extern const empty_namespacet empty_namespace; + +#endif // CPROVER_TESTING_UTILS_EMPTY_NAMESPACE_H From 5f46c9a1ca64a4138c5e04021fe05a52ca8ad6ad Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 30 Apr 2026 10:35:18 +0000 Subject: [PATCH 3/6] Use empty_namespace in unit tests Replace boilerplate 'symbol_tablet symbol_table; namespacet ns{symbol_table};' with 'auto &ns = empty_namespace;' (or the const variant) across 55 unit test files where the symbol table was never populated. In cases where the namespace variable was entirely unused, both the symbol_tablet and namespacet declarations are removed. Co-authored-by: Kiro --- unit/analyses/ai/ai_simplify_lhs.cpp | 18 ++- .../does_expr_lose_const.cpp | 4 +- .../does_type_preserve_const_correctness.cpp | 12 +- .../is_type_at_least_as_const_as.cpp | 12 +- .../abstract_environment/to_predicate.cpp | 5 +- .../abstract_object/index_range.cpp | 11 +- .../abstract_object/merge.cpp | 5 +- .../constant_abstract_value/meet.cpp | 5 +- .../constant_abstract_value/merge.cpp | 5 +- .../constant_abstract_value/to_predicate.cpp | 5 +- .../to_predicate.cpp | 5 +- .../eval-member-access.cpp | 5 +- .../maximum_length.cpp | 12 +- .../full_array_abstract_object/merge.cpp | 17 ++- .../to_predicate.cpp | 10 +- .../full_struct_abstract_object/merge.cpp | 15 ++- .../to_predicate.cpp | 9 +- .../extremes-go-top.cpp | 6 +- .../interval_abstract_value/meet.cpp | 5 +- .../interval_abstract_value/merge.cpp | 5 +- .../interval_abstract_value/to_predicate.cpp | 5 +- .../widening_merge.cpp | 5 +- .../value_expression_evaluation/assume.cpp | 5 +- .../assume_prune.cpp | 5 +- .../expression_evaluation.cpp | 5 +- .../value_set_abstract_object/compacting.cpp | 6 +- .../extremes-go-top.cpp | 6 +- .../value_set_abstract_object/meet.cpp | 5 +- .../value_set_abstract_object/merge.cpp | 6 +- .../to_predicate.cpp | 5 +- .../widening_merge.cpp | 5 +- .../to_predicate.cpp | 5 +- .../to_predicate.cpp | 5 +- .../variable_sensitivity_test_helpers.cpp | 7 +- unit/ansi-c/expr2c.cpp | 20 ++-- unit/goto-programs/goto_trace_output.cpp | 5 +- unit/goto-programs/xml_expr.cpp | 9 +- unit/goto-symex/is_constant.cpp | 5 +- unit/goto-symex/shadow_memory_util.cpp | 35 +++--- unit/solvers/bdd/miniBDD/miniBDD.cpp | 33 ++---- unit/solvers/flattening/boolbv.cpp | 5 +- .../solvers/flattening/boolbv_enumeration.cpp | 5 +- unit/solvers/flattening/boolbv_onehot.cpp | 5 +- unit/solvers/flattening/boolbv_update_bit.cpp | 5 +- unit/solvers/prop/bdd_expr.cpp | 10 +- .../smt2_incremental/convert_expr_to_smt.cpp | 26 ++-- .../smt2_incremental/object_tracking.cpp | 10 +- .../get_numeric_value_from_character.cpp | 12 +- .../is_digit_with_radix.cpp | 12 +- .../length_for_format_specifier.cpp | 14 +-- .../length_of_decimal_int.cpp | 9 +- .../string_refinement/string_refinement.cpp | 13 +- unit/testing-utils/empty_namespace.cpp | 2 +- unit/util/bitvector_expr.cpp | 5 +- unit/util/interval/add.cpp | 9 +- unit/util/interval/comparisons.cpp | 9 +- unit/util/interval/get_extreme.cpp | 5 +- unit/util/interval/modulo.cpp | 9 +- unit/util/interval/multiply.cpp | 9 +- unit/util/interval/subtract.cpp | 9 +- unit/util/lower_byte_operators.cpp | 11 +- unit/util/pointer_offset_size.cpp | 12 +- unit/util/simplify_expr.cpp | 111 +++++------------- unit/util/std_expr.cpp | 9 +- 64 files changed, 252 insertions(+), 427 deletions(-) diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index 7e38f26f392..8384f46c4c4 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -9,21 +9,18 @@ Author: Diffblue Ltd. /// \file /// Unit tests for ai_domain_baset::ai_simplify_lhs -#include -#include - -#include - -#include - #include #include #include -#include #include -#include #include +#include +#include +#include +#include +#include + class constant_simplification_mockt:public ai_domain_baset { public: @@ -74,8 +71,7 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs", { ansi_c_languaget language; - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; constant_simplification_mockt mock_ai_domain; diff --git a/unit/analyses/does_remove_const/does_expr_lose_const.cpp b/unit/analyses/does_remove_const/does_expr_lose_const.cpp index 91b48bb592d..7b700922d3b 100644 --- a/unit/analyses/does_remove_const/does_expr_lose_const.cpp +++ b/unit/analyses/does_remove_const/does_expr_lose_const.cpp @@ -14,20 +14,18 @@ Author: Diffblue Ltd. #include #include #include -#include #include #include #include #include +#include #include SCENARIO("does_expr_lose_const", "[core][analyses][does_remove_const][does_expr_remove_const]") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); goto_programt program; does_remove_constt does_remove_const(program); does_remove_const_testt does_remove_const_test(does_remove_const); diff --git a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp index 6dde902a93d..450c561346c 100644 --- a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp +++ b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp @@ -9,25 +9,21 @@ Author: Diffblue Ltd. /// \file /// Does Remove Const Unit Tests -#include - #include #include #include -#include - -#include #include -#include #include +#include +#include +#include +#include SCENARIO("does_type_preserve_const_correctness", "[core][analyses][does_remove_const][does_type_preserve_const_correctness]") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); goto_programt program; does_remove_constt does_remove_const(program); does_remove_const_testt does_remove_const_test(does_remove_const); diff --git a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp index 0771edf69e9..7b9de00d26f 100644 --- a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp +++ b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp @@ -9,25 +9,21 @@ Author: Diffblue Ltd. /// \file /// Does Remove Const Unit Tests -#include - #include #include #include -#include - -#include #include -#include #include +#include +#include +#include +#include SCENARIO("is_type_at_least_as_const", "[core][analyses][does_remove_const][is_type_at_least_as_const]") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); goto_programt program; does_remove_constt does_remove_const(program); does_remove_const_testt does_remove_const_test(does_remove_const); diff --git a/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp b/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp index c53ac49c2ac..ef9257e6fa0 100644 --- a/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp @@ -9,11 +9,11 @@ #include #include #include -#include #include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -28,8 +28,7 @@ SCENARIO( config.context_tracking.last_write_context = false; auto object_factory = variable_sensitivity_object_factoryt::configured_with(config); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("an abstract environment") { diff --git a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp index 31a30119f05..4e5f44b26b2 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp @@ -9,13 +9,13 @@ #include #include #include -#include #include #include #include #include #include +#include #include #include "analyses/variable-sensitivity/variable_sensitivity_test_helpers.h" @@ -30,8 +30,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt env{object_factory}; env.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("an integer constant has an index_range") { @@ -95,8 +94,7 @@ SCENARIO( vsd_configt::intervals()); abstract_environmentt env{object_factory}; env.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; auto type = signedbv_typet(32); GIVEN("a top intervals's range is empty") @@ -196,8 +194,7 @@ SCENARIO( vsd_configt::intervals()); abstract_environmentt env{object_factory}; env.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; auto type = signedbv_typet(32); GIVEN("a TOP value_set is empty") diff --git a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp index fb5b00fd275..2fc2be468c2 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include #include // NOLINTNEXTLINE(whitespace/line_length) @@ -93,8 +93,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; WHEN("merging TOP with 1") { diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp index 26b500e73cd..0ee4a750052 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -74,8 +74,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("meeting two constants") { diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index 10fffe551e5..7e9833ae6f1 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -9,11 +9,11 @@ #include #include #include -#include #include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -48,8 +48,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("merging two constants") { diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp index a5358355321..0b280e17976 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp @@ -9,12 +9,12 @@ #include #include #include -#include #include #include #include #include +#include #include SCENARIO( @@ -34,8 +34,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("constant_abstract_value") { diff --git a/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp index ce37c9ca7cc..d8441ca2196 100644 --- a/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp @@ -9,12 +9,12 @@ #include #include #include -#include #include #include #include #include +#include #include SCENARIO( @@ -35,8 +35,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("constant_pointer_abstract_object") { diff --git a/unit/analyses/variable-sensitivity/eval-member-access.cpp b/unit/analyses/variable-sensitivity/eval-member-access.cpp index 3fd4c3537ad..891300199b2 100644 --- a/unit/analyses/variable-sensitivity/eval-member-access.cpp +++ b/unit/analyses/variable-sensitivity/eval-member-access.cpp @@ -8,13 +8,13 @@ #include #include -#include #include #include #include #include #include +#include #include void test_array( @@ -33,8 +33,7 @@ SCENARIO( vsd_configt::constant_domain())}; environment.make_top(); // Domains are bottom on construction - symbol_tablet symbol_table; - namespacet ns{symbol_table}; + auto &ns = empty_namespace; GIVEN("An array of {1, 2, 3}") { diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp index 8ec9733cf23..4ff546de306 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp @@ -6,16 +6,15 @@ \*******************************************************************/ -#include "array_builder.h" +#include +#include #include #include - +#include #include -#include -#include -#include +#include "array_builder.h" using abstract_object_ptrt = std::shared_ptr; @@ -53,8 +52,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(configuration); abstract_environmentt environment(object_factory); environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; WHEN("maximum size is " + std::to_string(max_array_index)) { WHEN("array = {1, 2, 3}, writes under maximum size") diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp index 140279e4855..e42d3bae669 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp @@ -6,20 +6,20 @@ \*******************************************************************/ -#include -#include +#include +#include +#include +#include #include #include #include #include #include +#include +#include -#include -#include -#include -#include -#include +#include SCENARIO( "merge_constant_array_abstract_object", @@ -47,8 +47,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt environment(object_factory); environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; WHEN("Merging two constant array AOs with the same array") { diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp index 263244fcbc1..55759c6509e 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp @@ -7,15 +7,12 @@ \*******************************************************************/ #include -#include - #include +#include #include - +#include #include -#include - SCENARIO( "array to predicate", "[core][analyses][variable-sensitivity][full_array_abstract_object][to_" @@ -25,8 +22,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt environment(object_factory); environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("full_array_abstract_object to predicate") { diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp index 4efe8b4f6ba..48f069f702c 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp @@ -6,19 +6,19 @@ \*******************************************************************/ -#include -#include +#include +#include +#include #include #include #include #include #include +#include +#include -#include -#include -#include -#include +#include SCENARIO( "merge_full_struct_abstract_object", @@ -45,8 +45,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt environment(object_factory); environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; WHEN("Merging two constant struct AOs with the same contents") { diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp index 2ad91a4e383..3cee65819c9 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp @@ -7,14 +7,12 @@ \*******************************************************************/ #include -#include - #include +#include #include +#include #include -#include - SCENARIO( "struct to predicate", "[core][analyses][variable-sensitivity][full_struct_abstract_object][to_" @@ -24,8 +22,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt environment(object_factory); environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("full_struct_abstract_object to predicate") { diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp index be191ecfc9f..abbcfa20de3 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp @@ -8,8 +8,6 @@ #include #include -#include -#include #include #include @@ -17,6 +15,7 @@ // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep #include +#include #include static void verify_extreme_interval( @@ -39,8 +38,7 @@ SCENARIO( auto environment = abstract_environmentt{object_factory}; environment.make_top(); - auto symbol_table = symbol_tablet{}; - auto ns = namespacet{symbol_table}; + auto &ns = empty_namespace; GIVEN("[min-max] signed goes TOP") { diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp index 8d2d97029d4..84cd99c8491 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include #include // NOLINTNEXTLINE(whitespace/line_length) @@ -86,8 +86,7 @@ SCENARIO( abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("meeting two intervals") { diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp index 8951fd2c0d8..f6ec64cc24b 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -52,8 +52,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("merging two intervals") { diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp index 91941c97dd7..8fb084be827 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -44,8 +44,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("interval_abstract_value") { diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp index 4f0a7bdfd73..fbd89178eea 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -60,8 +60,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("interval merges which don't widen") { diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp index f26e0da09b5..a6745ae9d9b 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -170,8 +170,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; assume_testert assumeTester(environment, ns); diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp index 18c7e0b86ca..1f41f8f1856 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp @@ -9,11 +9,11 @@ #include #include #include -#include #include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -81,8 +81,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; auto type = signedbv_typet(32); auto val0 = from_integer(0, type); diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp index a33d432cb3f..355a1f32ab5 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -44,8 +44,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("adding two constants") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp index 1baefda7468..170dbabf9cd 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp @@ -13,8 +13,6 @@ #include #include -#include -#include #include #include @@ -22,6 +20,7 @@ // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep #include +#include #include SCENARIO( @@ -52,8 +51,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); auto environment = abstract_environmentt{object_factory}; environment.make_top(); - auto symbol_table = symbol_tablet{}; - auto ns = namespacet{symbol_table}; + auto &ns = empty_namespace; GIVEN("compact values into existing interval") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp index 32d87327c6d..c1a99fef46e 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp @@ -8,8 +8,6 @@ #include #include -#include -#include #include @@ -17,6 +15,7 @@ #include // IWYU pragma: keep #include #include +#include #include SCENARIO( @@ -28,8 +27,7 @@ SCENARIO( auto environment = abstract_environmentt{object_factory}; environment.make_top(); - auto symbol_table = symbol_tablet{}; - auto ns = namespacet{symbol_table}; + auto &ns = empty_namespace; GIVEN("{FALSE, TRUE} goes TOP") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp index e354520d407..4495e6bb77a 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include #include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -76,8 +76,7 @@ SCENARIO( abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("meeting two value_sets") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp index 31eb26d9148..1fd4edd60f2 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp @@ -8,8 +8,6 @@ #include #include -#include -#include #include @@ -24,6 +22,7 @@ // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep #include +#include #include static merge_result @@ -50,8 +49,7 @@ SCENARIO( vsd_configt::value_set()); auto environment = abstract_environmentt{object_factory}; environment.make_top(); - auto symbol_table = symbol_tablet{}; - auto ns = namespacet{symbol_table}; + auto &ns = empty_namespace; GIVEN("merging two value sets") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp index e37287e2b30..f612e5496cd 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -46,8 +46,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("value_set_abstract_object") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp index 8f85268795d..9ecc59a2e82 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp @@ -9,10 +9,10 @@ #include #include #include -#include #include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep @@ -68,8 +68,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("value_set merges which don't widen") { diff --git a/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp index ed8cf002a4d..6ba46fb0f4f 100644 --- a/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp @@ -9,9 +9,9 @@ #include #include #include -#include #include +#include // NOLINTNEXTLINE(whitespace/line_length) #include // IWYU pragma: keep #include @@ -44,8 +44,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("value_set_pointer_abstract_object") { diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp index aa149ae0383..fc16bce44e4 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp @@ -9,11 +9,11 @@ #include #include #include -#include #include #include #include +#include #include SCENARIO( @@ -26,8 +26,7 @@ SCENARIO( config.context_tracking.last_write_context = false; auto object_factory = variable_sensitivity_object_factoryt::configured_with(config); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; GIVEN("to_predicate()") { diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 07e0a7437c2..46a29323af5 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -11,9 +11,7 @@ #include #include #include -#include #include -#include #include #include @@ -21,6 +19,7 @@ #include #include #include +#include #include std::shared_ptr @@ -182,12 +181,10 @@ std::string expr_to_str(const exprt &expr) if(expr.id() == ID_min_value) return "min"; - auto st = symbol_tablet{}; - auto ns = namespacet{st}; auto expr_str = std::string{}; auto lang = new_ansi_c_language(); - lang->from_expr(expr, expr_str, ns); + lang->from_expr(expr, expr_str, empty_namespace); return expr_str; } diff --git a/unit/ansi-c/expr2c.cpp b/unit/ansi-c/expr2c.cpp index cfbed21dcb4..4f48d1dbb0e 100644 --- a/unit/ansi-c/expr2c.cpp +++ b/unit/ansi-c/expr2c.cpp @@ -6,23 +6,21 @@ Author: Diffblue \*******************************************************************/ -#include -#include #include #include #include #include -#include -#include + +#include +#include +#include TEST_CASE("rol_2_c_conversion_unsigned", "[core][ansi-c][expr2c]") { auto lhs = from_integer(31, unsignedbv_typet(32)); auto rhs = from_integer(3, unsignedbv_typet(32)); auto rol = shift_exprt(lhs, ID_rol, rhs); - CHECK( - expr2c(rol, namespacet{symbol_tablet{}}) == - "31 << 3 % 32 | 31 >> 32 - 3 % 32"); + CHECK(expr2c(rol, empty_namespace) == "31 << 3 % 32 | 31 >> 32 - 3 % 32"); } TEST_CASE("rol_2_c_conversion_signed", "[core][ansi-c][expr2c]") @@ -37,7 +35,7 @@ TEST_CASE("rol_2_c_conversion_signed", "[core][ansi-c][expr2c]") auto rhs = from_integer(3, signedbv_typet(8)); auto rol = shift_exprt(lhs, ID_rol, rhs); CHECK( - expr2c(rol, namespacet{symbol_tablet{}}) == + expr2c(rol, empty_namespace) == "(unsigned char)31 << 3 % 8 | (unsigned char)31 >> 8 - 3 % 8"); } @@ -46,9 +44,7 @@ TEST_CASE("ror_2_c_conversion_unsigned", "[core][ansi-c][expr2c]") auto lhs = from_integer(31, unsignedbv_typet(32)); auto rhs = from_integer(3, unsignedbv_typet(32)); auto ror = shift_exprt(lhs, ID_ror, rhs); - CHECK( - expr2c(ror, namespacet{symbol_tablet{}}) == - "31 >> 3 % 32 | 31 << 32 - 3 % 32"); + CHECK(expr2c(ror, empty_namespace) == "31 >> 3 % 32 | 31 << 32 - 3 % 32"); } TEST_CASE("ror_2_c_conversion_signed", "[core][ansi-c][expr2c]") @@ -63,6 +59,6 @@ TEST_CASE("ror_2_c_conversion_signed", "[core][ansi-c][expr2c]") auto rhs = from_integer(3, integer_bitvector_typet(ID_signedbv, 32)); auto ror = shift_exprt(lhs, ID_ror, rhs); CHECK( - expr2c(ror, namespacet{symbol_tablet{}}) == + expr2c(ror, empty_namespace) == "(unsigned int)31 >> 3 % 32 | (unsigned int)31 << 32 - 3 % 32"); } diff --git a/unit/goto-programs/goto_trace_output.cpp b/unit/goto-programs/goto_trace_output.cpp index 729d5ca2b50..e6b6045caab 100644 --- a/unit/goto-programs/goto_trace_output.cpp +++ b/unit/goto-programs/goto_trace_output.cpp @@ -7,11 +7,11 @@ Author: Diffblue Ltd. \*******************************************************************/ #include -#include #include #include +#include #include #include @@ -20,8 +20,7 @@ SCENARIO( "Output trace with nil lhs object", "[core][goto-programs][goto_trace]") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; goto_programt::instructionst instructions; instructions.emplace_back(goto_program_instruction_typet::OTHER); goto_trace_stept step; diff --git a/unit/goto-programs/xml_expr.cpp b/unit/goto-programs/xml_expr.cpp index dac9d344111..20971950bc9 100644 --- a/unit/goto-programs/xml_expr.cpp +++ b/unit/goto-programs/xml_expr.cpp @@ -6,22 +6,21 @@ Author: Michael Tautschnig \*******************************************************************/ -#include - #include #include #include #include -#include #include +#include +#include + TEST_CASE("Constant expression to XML") { config.set_arch("none"); - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); + const auto &ns = empty_namespace; const constant_exprt number_ubv = from_integer(0xFF, unsignedbv_typet(8)); const xmlt x_ubv = xml(number_ubv, ns); diff --git a/unit/goto-symex/is_constant.cpp b/unit/goto-symex/is_constant.cpp index 29bb54a7d6f..e606354ed55 100644 --- a/unit/goto-symex/is_constant.cpp +++ b/unit/goto-symex/is_constant.cpp @@ -9,15 +9,14 @@ Author: Diffblue Ltd. #include #include #include -#include #include +#include #include SCENARIO("goto-symex-is-constant", "[core][goto-symex][is_constant]") { - symbol_tablet symbol_table; - namespacet ns{symbol_table}; + auto &ns = empty_namespace; signedbv_typet int_type(32); constant_exprt sizeof_constant("4", int_type); diff --git a/unit/goto-symex/shadow_memory_util.cpp b/unit/goto-symex/shadow_memory_util.cpp index 1d315aa5d5b..05fe8720725 100644 --- a/unit/goto-symex/shadow_memory_util.cpp +++ b/unit/goto-symex/shadow_memory_util.cpp @@ -10,17 +10,16 @@ #include #include +#include #include +#include #include /// Helper struct to hold useful test components. struct shadow_memory_util_test_environmentt { - symbol_tablet symbol_table; - namespacet ns{symbol_table}; source_locationt loc{}; - null_message_handlert null_message_handler{}; messaget log{null_message_handler}; static shadow_memory_util_test_environmentt make() @@ -183,9 +182,9 @@ TEST_CASE( unsignedbv_typet{56}); const exprt max_over_struct = - compute_max_over_bytes(bitvector, sm_type, test.ns); + compute_max_over_bytes(bitvector, sm_type, empty_namespace); - const exprt simplified = simplify_expr(max_over_struct, test.ns); + const exprt simplified = simplify_expr(max_over_struct, empty_namespace); REQUIRE(simplified == from_integer(max(values), sm_type)); } @@ -204,9 +203,9 @@ TEST_CASE( const array_exprt array_expr{array_operands, array_type}; const exprt max_over_struct = - compute_max_over_bytes(array_expr, sm_type, test.ns); + compute_max_over_bytes(array_expr, sm_type, empty_namespace); - const exprt simplified = simplify_expr(max_over_struct, test.ns); + const exprt simplified = simplify_expr(max_over_struct, empty_namespace); REQUIRE(simplified == from_integer(max(values), sm_type)); } @@ -231,9 +230,9 @@ TEST_CASE( const struct_exprt struct_expr{struct_operands, struct_type}; const exprt max_over_struct = - compute_max_over_bytes(struct_expr, sm_type, test.ns); + compute_max_over_bytes(struct_expr, sm_type, empty_namespace); - const exprt simplified = simplify_expr(max_over_struct, test.ns); + const exprt simplified = simplify_expr(max_over_struct, empty_namespace); REQUIRE(simplified == from_integer(max(values), sm_type)); } @@ -299,11 +298,11 @@ TEST_CASE( (values[4] << 32) + (values[5] << 40) + (values[6] << 48), unsignedbv_typet{56}); - const exprt max_over_struct = - compute_or_over_bytes(bitvector, sm_type, test.ns, test.log, false); + const exprt max_over_struct = compute_or_over_bytes( + bitvector, sm_type, empty_namespace, test.log, false); const exprt simplified = - simplify_bit_or_exprt(simplify_expr(max_over_struct, test.ns)); + simplify_bit_or_exprt(simplify_expr(max_over_struct, empty_namespace)); REQUIRE(simplified == from_integer(compute_or(values), sm_type)); } @@ -321,11 +320,11 @@ TEST_CASE( from_integer(values[6], unsigned_char_type())}; const array_exprt array_expr{array_operands, array_type}; - const exprt max_over_struct = - compute_or_over_bytes(array_expr, sm_type, test.ns, test.log, false); + const exprt max_over_struct = compute_or_over_bytes( + array_expr, sm_type, empty_namespace, test.log, false); const exprt simplified = - simplify_bit_or_exprt(simplify_expr(max_over_struct, test.ns)); + simplify_bit_or_exprt(simplify_expr(max_over_struct, empty_namespace)); REQUIRE(simplified == from_integer(compute_or(values), sm_type)); } @@ -349,11 +348,11 @@ TEST_CASE( from_integer(fizz, char_type()), inner_struct_expr}; const struct_exprt struct_expr{struct_operands, struct_type}; - const exprt max_over_struct = - compute_or_over_bytes(struct_expr, sm_type, test.ns, test.log, false); + const exprt max_over_struct = compute_or_over_bytes( + struct_expr, sm_type, empty_namespace, test.log, false); const exprt simplified = - simplify_bit_or_exprt(simplify_expr(max_over_struct, test.ns)); + simplify_bit_or_exprt(simplify_expr(max_over_struct, empty_namespace)); REQUIRE(simplified == from_integer(compute_or(values), sm_type)); } diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp index 71a311e31a9..f5da98eee69 100644 --- a/unit/solvers/bdd/miniBDD/miniBDD.cpp +++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp @@ -9,20 +9,19 @@ Author: Diffblue Ltd. /// \file /// Unit tests for miniBDD -#include -#include - -#include -#include -#include - #include #include #include #include #include #include -#include + +#include +#include +#include +#include +#include +#include class bdd_propt : public propt { @@ -202,8 +201,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x&!x==0") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); boolbvt boolbv(ns, bdd_prop, null_message_handler); @@ -220,8 +218,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x+x==1") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); boolbvt boolbv(ns, bdd_prop, null_message_handler); @@ -237,8 +234,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*y==y*x") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); boolbvt boolbv(ns, bdd_prop, null_message_handler); @@ -255,8 +251,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*x==2") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); boolbvt boolbv(ns, bdd_prop, null_message_handler); @@ -272,8 +267,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*x==4") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); boolbvt boolbv(ns, bdd_prop, null_message_handler); @@ -334,9 +328,6 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") or_exprt o(and_exprt(a, b), not_exprt(a)); - symbol_tablet symbol_table; - namespacet ns(symbol_table); - { std::ostringstream oss; oss << format(o); diff --git a/unit/solvers/flattening/boolbv.cpp b/unit/solvers/flattening/boolbv.cpp index a3ca65f32f5..1ef4e6d31dd 100644 --- a/unit/solvers/flattening/boolbv.cpp +++ b/unit/solvers/flattening/boolbv.cpp @@ -14,10 +14,10 @@ Author: Daniel Kroening #include #include #include -#include #include #include +#include #include SCENARIO("boolbvt", "[core][solvers][flattening][boolbvt]") @@ -28,8 +28,7 @@ SCENARIO("boolbvt", "[core][solvers][flattening][boolbvt]") GIVEN("A satisfiable bit-vector formula f") { satcheckt satcheck(message_handler); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; boolbvt boolbv(ns, satcheck, message_handler); unsignedbv_typet u32(32); diff --git a/unit/solvers/flattening/boolbv_enumeration.cpp b/unit/solvers/flattening/boolbv_enumeration.cpp index 521d99e8108..6571ceea591 100644 --- a/unit/solvers/flattening/boolbv_enumeration.cpp +++ b/unit/solvers/flattening/boolbv_enumeration.cpp @@ -10,10 +10,10 @@ Author: Daniel Kroening, dkr@amazon.com #include #include -#include #include #include +#include #include TEST_CASE( @@ -23,8 +23,7 @@ TEST_CASE( console_message_handlert message_handler; message_handler.set_verbosity(0); satcheckt satcheck{message_handler}; - symbol_tablet symbol_table; - namespacet ns{symbol_table}; + auto &ns = empty_namespace; boolbvt boolbv{ns, satcheck, message_handler}; enumeration_typet enumeration; enumeration.elements().push_back(irept{"A"}); diff --git a/unit/solvers/flattening/boolbv_onehot.cpp b/unit/solvers/flattening/boolbv_onehot.cpp index c2ee0d45fcb..9ac154ffc65 100644 --- a/unit/solvers/flattening/boolbv_onehot.cpp +++ b/unit/solvers/flattening/boolbv_onehot.cpp @@ -14,10 +14,10 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include -#include #include #include +#include #include TEST_CASE("onehot flattening", "[core][solvers][flattening][boolbvt][onehot]") @@ -25,8 +25,7 @@ TEST_CASE("onehot flattening", "[core][solvers][flattening][boolbvt][onehot]") console_message_handlert message_handler; message_handler.set_verbosity(0); satcheckt satcheck{message_handler}; - symbol_tablet symbol_table; - namespacet ns{symbol_table}; + auto &ns = empty_namespace; boolbvt boolbv{ns, satcheck, message_handler}; unsignedbv_typet u8{8}; diff --git a/unit/solvers/flattening/boolbv_update_bit.cpp b/unit/solvers/flattening/boolbv_update_bit.cpp index b8b13336798..92530c78e4a 100644 --- a/unit/solvers/flattening/boolbv_update_bit.cpp +++ b/unit/solvers/flattening/boolbv_update_bit.cpp @@ -15,10 +15,10 @@ Author: Daniel Kroening #include #include #include -#include #include #include +#include #include SCENARIO( @@ -31,8 +31,7 @@ SCENARIO( GIVEN("A satisfiable bit-vector formula f with update_bit") { satcheckt satcheck{message_handler}; - symbol_tablet symbol_table; - namespacet ns{symbol_table}; + auto &ns = empty_namespace; boolbvt boolbv{ns, satcheck, message_handler}; unsignedbv_typet u32{32}; diff --git a/unit/solvers/prop/bdd_expr.cpp b/unit/solvers/prop/bdd_expr.cpp index 3567b34e4fd..e84672c9e7c 100644 --- a/unit/solvers/prop/bdd_expr.cpp +++ b/unit/solvers/prop/bdd_expr.cpp @@ -9,17 +9,15 @@ Author: Diffblue Ltd. /// \file /// Unit tests for bdd_expr -#include - -#include #include #include -#include + +#include +#include +#include SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]") { - symbol_tablet symbol_table; - namespacet ns{symbol_table}; bdd_exprt bdd_expr_converter; GIVEN("A bdd for x&!x") diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index ec94f96b9ea..49b1cbcefe0 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -9,7 +9,6 @@ #include #include #include -#include #include #include @@ -19,6 +18,7 @@ #include #include #include +#include #include #include @@ -469,8 +469,7 @@ TEST_CASE( { // (int32_t *)a + 2 const auto pointer_arith_expr = plus_exprt{pointer_a, two_bvint_32bit}; - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; track_expression_objects(pointer_arith_expr, ns, test.object_map); associate_pointer_sizes( pointer_arith_expr, @@ -545,8 +544,7 @@ TEST_CASE( // (int *)a - 2 is coming to us as (int *)a + (-2), so a design decision // was made to handle only that form. const auto pointer_arith_expr = plus_exprt{pointer_a, minus_two_bvint}; - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; track_expression_objects(pointer_arith_expr, ns, test.object_map); associate_pointer_sizes( pointer_arith_expr, @@ -577,8 +575,7 @@ TEST_CASE( const auto two_bvint = from_integer(2, signedbv_typet{pointer_width}); const auto pointer_arith_expr = minus_exprt{pointer_a, two_bvint}; - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; track_expression_objects(pointer_arith_expr, ns, test.object_map); associate_pointer_sizes( pointer_arith_expr, @@ -615,8 +612,7 @@ TEST_CASE( { // (int32_t *)a - (int32_t *)b const auto pointer_subtraction = minus_exprt{pointer_b, pointer_a}; - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; track_expression_objects(pointer_subtraction, ns, test.object_map); associate_pointer_sizes( pointer_subtraction, @@ -1471,8 +1467,7 @@ TEST_CASE( { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64); - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; const symbol_exprt foo{"foo", unsignedbv_typet{32}}; const symbol_exprt bar{"bar", unsignedbv_typet{32}}; SECTION("Address of symbol") @@ -1674,8 +1669,7 @@ TEST_CASE( { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64); - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; const symbol_exprt foo{"foo", unsignedbv_typet{32}}; const object_size_exprt object_size{ address_of_exprt{foo}, unsignedbv_typet{64}}; @@ -1699,8 +1693,7 @@ TEST_CASE( { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64); - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; const symbol_exprt foo{"foo", unsignedbv_typet{32}}; const is_dynamic_object_exprt is_dynamic_object{address_of_exprt{foo}}; track_expression_objects(is_dynamic_object, ns, test.object_map); @@ -1723,8 +1716,7 @@ TEST_CASE( { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64); - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; const typet value_type = signedbv_typet{8}; const exprt array = symbol_exprt{ "my_array", array_typet{value_type, from_integer(10, signed_size_type())}}; diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index 910863f805d..c7793fb4052 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -9,6 +9,7 @@ #include #include +#include #include #include @@ -135,13 +136,11 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]") actual_invalid_object_pointer->second.base_expression == invalid_object_pointer); } - symbol_tablet symbol_table; - namespacet ns{symbol_table}; SECTION("Check objects of compound expression not yet tracked") { CHECK_FALSE(objects_are_already_tracked(compound_expression, object_map)); } - track_expression_objects(compound_expression, ns, object_map); + track_expression_objects(compound_expression, empty_namespace, object_map); SECTION("Tracking expression objects") { CHECK(object_map.size() == 5); @@ -212,8 +211,6 @@ TEST_CASE("Tracking dynamic object status.", "[core][smt2_incremental]") config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; config.ansi_c.set_arch_spec_x86_64(); smt_object_mapt object_map = initial_smt_object_map(); - symbol_tablet symbol_table; - namespacet ns{symbol_table}; exprt base_object; bool expected_dynamic_status; using rowt = @@ -224,7 +221,8 @@ TEST_CASE("Tracking dynamic object status.", "[core][smt2_incremental]") rowt{symbol_exprt{SYMEX_DYNAMIC_PREFIX "bar", unsignedbv_typet{8}}, true}, rowt{from_integer(42, make_type_dynamic(signedbv_typet{16})), true}); INFO("base_object is - " + base_object.pretty(1, 0)); - track_expression_objects(address_of_exprt{base_object}, ns, object_map); + track_expression_objects( + address_of_exprt{base_object}, empty_namespace, object_map); const auto object = object_map.find(base_object); REQUIRE(object != object_map.end()); REQUIRE(object->second.is_dynamic == expected_dynamic_status); diff --git a/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp index ea4b9b139f3..0531ca3ed38 100644 --- a/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp +++ b/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp @@ -7,13 +7,12 @@ Author: Diffblue Ltd. \*******************************************************************/ -#include - -#include - #include #include -#include + +#include +#include +#include /// Get the simplified return value of get_numeric_value_from_character called /// with a radix @@ -25,8 +24,7 @@ static exprt actual( const unsigned long radix_ul) { const constant_exprt chr = from_integer(character, char_type); - symbol_tablet symtab; - const namespacet ns(symtab); + const auto &ns = empty_namespace; return simplify_expr( get_numeric_value_from_character( chr, char_type, int_type, strict_formatting, radix_ul), diff --git a/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp index f4833a812ab..8feada5927d 100644 --- a/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp +++ b/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp @@ -7,13 +7,12 @@ Author: Diffblue Ltd. \*******************************************************************/ -#include - -#include - #include #include -#include + +#include +#include +#include /// Get the simplified return value of is_digit_with_radix called with a radix static exprt actual( @@ -24,8 +23,7 @@ static exprt actual( { const typet char_type = unsignedbv_typet(16); const constant_exprt chr = from_integer(int_value, char_type); - symbol_tablet symtab; - const namespacet ns(symtab); + const auto &ns = empty_namespace; return simplify_expr( is_digit_with_radix( diff --git a/unit/solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp b/unit/solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp index 8148114e727..30cb193952c 100644 --- a/unit/solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp +++ b/unit/solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp @@ -7,16 +7,15 @@ Author: Diffblue Ltd. \*******************************************************************/ -#include - -#include -#include - #include #include #include #include -#include + +#include +#include +#include +#include // Create array_string_exprt from array of characters array_string_exprt from_char_vector( @@ -49,8 +48,7 @@ SCENARIO( const std::size_t pointer_width = 16; const auto pointer_type = pointer_typet(char_type, pointer_width); - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; symbol_generatort fresh_symbol; array_poolt array_pool{fresh_symbol}; diff --git a/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp b/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp index d2afe05f39b..3ab805dec4c 100644 --- a/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp +++ b/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp @@ -7,11 +7,11 @@ Author: Diffblue Ltd. \*******************************************************************/ -#include +#include #include -#include -#include +#include +#include SCENARIO( "length_of_decimal_int", @@ -19,8 +19,7 @@ SCENARIO( { const typet type = signedbv_typet(32); - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + const auto &ns = empty_namespace; const std::vector input_values = { 0, 1, 10, 15, 999, 1000000001, -1, -21111111, -1234567890}; diff --git a/unit/solvers/strings/string_refinement/string_refinement.cpp b/unit/solvers/strings/string_refinement/string_refinement.cpp index d86abcec0e5..e9353bcc9a9 100644 --- a/unit/solvers/strings/string_refinement/string_refinement.cpp +++ b/unit/solvers/strings/string_refinement/string_refinement.cpp @@ -7,16 +7,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com \*******************************************************************/ -#include - -#include -#include #include #include #include #include #include -#include + +#include +#include +#include +#include SCENARIO("string refinement", "[core][solvers][strings][string_refinement]") { @@ -27,8 +27,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]") null_message_handlert log{}; info.message_handler = &log; - symbol_tablet symbol_table; - namespacet ns{symbol_table}; + auto &ns = empty_namespace; info.ns = &ns; satcheckt sat_solver{log}; diff --git a/unit/testing-utils/empty_namespace.cpp b/unit/testing-utils/empty_namespace.cpp index 0513ef483f9..ac9ab758521 100644 --- a/unit/testing-utils/empty_namespace.cpp +++ b/unit/testing-utils/empty_namespace.cpp @@ -9,6 +9,6 @@ Author: Diffblue Limited. /// \file /// Global instance of \ref empty_namespacet. -#include "empty_namespacet.h" +#include "empty_namespace.h" const empty_namespacet empty_namespace; diff --git a/unit/util/bitvector_expr.cpp b/unit/util/bitvector_expr.cpp index bf4207fa11f..82aa4ee98cd 100644 --- a/unit/util/bitvector_expr.cpp +++ b/unit/util/bitvector_expr.cpp @@ -6,10 +6,10 @@ #include #include #include -#include #include #include +#include #include TEST_CASE( @@ -77,8 +77,7 @@ TEST_CASE("onehot expression lowering", "[core][util][expr]") console_message_handlert message_handler; message_handler.set_verbosity(0); satcheckt satcheck{message_handler}; - symbol_tablet symbol_table; - namespacet ns{symbol_table}; + auto &ns = empty_namespace; boolbvt boolbv{ns, satcheck, message_handler}; unsignedbv_typet u8{8}; diff --git a/unit/util/interval/add.cpp b/unit/util/interval/add.cpp index 45699877759..a7d6dd8e916 100644 --- a/unit/util/interval/add.cpp +++ b/unit/util/interval/add.cpp @@ -3,13 +3,13 @@ Author: DiffBlue Limited \*******************************************************************/ -#include - #include #include #include #include -#include + +#include +#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) @@ -19,9 +19,6 @@ SCENARIO("add interval domain", "[core][analyses][interval][add]") { GIVEN("Two simple signed intervals") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); - WHEN("Both are positive [2,4]+[6,8]") { constant_interval_exprt left(CEV(2), CEV(4)); diff --git a/unit/util/interval/comparisons.cpp b/unit/util/interval/comparisons.cpp index e31159a20d2..9402df62e95 100644 --- a/unit/util/interval/comparisons.cpp +++ b/unit/util/interval/comparisons.cpp @@ -3,13 +3,13 @@ Author: DiffBlue Limited \*******************************************************************/ -#include - #include #include #include #include -#include + +#include +#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) @@ -19,9 +19,6 @@ SCENARIO("comparison interval domain", "[core][analyses][interval][comparison]") { GIVEN("Two simple signed intervals") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); - WHEN("<, >, <=, >=, ==, != are tested on expressions") { THEN("Require correctness") diff --git a/unit/util/interval/get_extreme.cpp b/unit/util/interval/get_extreme.cpp index 58d6249859d..5d772530b8b 100644 --- a/unit/util/interval/get_extreme.cpp +++ b/unit/util/interval/get_extreme.cpp @@ -9,8 +9,8 @@ #include #include #include -#include +#include #include #include @@ -23,8 +23,7 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]") { GIVEN("A selection of constant_exprts in a std::vector and map") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; std::vector ve; diff --git a/unit/util/interval/modulo.cpp b/unit/util/interval/modulo.cpp index 895a995c4c1..4872961740c 100644 --- a/unit/util/interval/modulo.cpp +++ b/unit/util/interval/modulo.cpp @@ -3,13 +3,13 @@ Author: DiffBlue Limited \*******************************************************************/ -#include - #include #include #include #include -#include + +#include +#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) @@ -38,9 +38,6 @@ SCENARIO("modulo interval domain", "[core][analyses][interval][modulo]") } GIVEN("Two simple signed intervals") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); - WHEN("Positive RHS") { THEN("Ensure result is consistent.") diff --git a/unit/util/interval/multiply.cpp b/unit/util/interval/multiply.cpp index 27274b47b16..48fdcbd3030 100644 --- a/unit/util/interval/multiply.cpp +++ b/unit/util/interval/multiply.cpp @@ -3,13 +3,13 @@ Author: DiffBlue Limited \*******************************************************************/ -#include - #include #include #include #include -#include + +#include +#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) @@ -19,9 +19,6 @@ SCENARIO("multiply interval domain", "[core][analyses][interval][multiply]") { GIVEN("A selection of constant_exprts in a std::vector and map") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); - WHEN("Single element multiplication") { constant_interval_exprt a = constant_interval_exprt::singleton(CEV(5)); diff --git a/unit/util/interval/subtract.cpp b/unit/util/interval/subtract.cpp index be9da78d21d..8790c25fd3e 100644 --- a/unit/util/interval/subtract.cpp +++ b/unit/util/interval/subtract.cpp @@ -3,13 +3,13 @@ Author: DiffBlue Limited \*******************************************************************/ -#include - #include #include #include #include -#include + +#include +#include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) #define V_(X) (bvrep2integer(X.c_str(), 32, true)) @@ -19,9 +19,6 @@ SCENARIO("subtract interval domain", "[core][analyses][interval][subtract]") { GIVEN("Two simple signed intervals") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); - WHEN("The result is positive [6,8]-[2,4]") { constant_interval_exprt left(CEV(6), CEV(8)); diff --git a/unit/util/lower_byte_operators.cpp b/unit/util/lower_byte_operators.cpp index 4f3ac9ba9be..155cb69213f 100644 --- a/unit/util/lower_byte_operators.cpp +++ b/unit/util/lower_byte_operators.cpp @@ -18,8 +18,8 @@ #include #include #include -#include +#include #include TEST_CASE("byte extract and bits", "[core][util][lowering][byte_extract]") @@ -29,8 +29,7 @@ TEST_CASE("byte extract and bits", "[core][util][lowering][byte_extract]") cmdlinet cmdline; config.set(cmdline); - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); + const auto &ns = empty_namespace; const unsignedbv_typet u16{16}; const exprt sixteen_bits = from_integer(0x1234, u16); @@ -99,8 +98,7 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]") cmdlinet cmdline; config.set(cmdline); - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); + const auto &ns = empty_namespace; GIVEN("A byte_extract over a POD") { @@ -367,8 +365,7 @@ SCENARIO("byte_update_lowering", "[core][util][lowering][byte_update]") cmdlinet cmdline; config.set(cmdline); - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); + const auto &ns = empty_namespace; GIVEN("A byte_update of a POD") { diff --git a/unit/util/pointer_offset_size.cpp b/unit/util/pointer_offset_size.cpp index a091f1c7f42..1da92d004e7 100644 --- a/unit/util/pointer_offset_size.cpp +++ b/unit/util/pointer_offset_size.cpp @@ -6,8 +6,6 @@ Author: Michael Tautschnig \*******************************************************************/ -#include - #include #include #include @@ -16,7 +14,9 @@ Author: Michael Tautschnig #include #include #include -#include + +#include +#include TEST_CASE("Build subexpression to access element at offset into array") { @@ -25,8 +25,7 @@ TEST_CASE("Build subexpression to access element at offset into array") cmdlinet cmdline; config.set(cmdline); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; const signedbv_typet t(32); @@ -84,8 +83,7 @@ TEST_CASE("Build subexpression to access element at offset into struct") cmdlinet cmdline; config.set(cmdline); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; const signedbv_typet t(32); diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 663b5b19325..e041ca4e07e 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -22,15 +22,13 @@ Author: Michael Tautschnig #include #include +#include #include TEST_CASE("Simplify pointer_offset(address of array index)", "[core][util]") { config.set_arch("none"); - symbol_tablet symbol_table; - namespacet ns(symbol_table); - array_typet array_type(char_type(), from_integer(2, size_type())); symbol_exprt array("A", array_type); index_exprt index(array, from_integer(1, c_index_type())); @@ -38,7 +36,7 @@ TEST_CASE("Simplify pointer_offset(address of array index)", "[core][util]") exprt p_o=pointer_offset(address_of); - exprt simp=simplify_expr(p_o, ns); + exprt simp = simplify_expr(p_o, empty_namespace); REQUIRE(simp.is_constant()); const mp_integer offset_value = @@ -53,24 +51,20 @@ TEST_CASE("Simplify byte extract", "[core][util]") cmdlinet cmdline; config.set(cmdline); - symbol_tablet symbol_table; - namespacet ns(symbol_table); - // byte-extracting type T at offset 0 from an object of type T yields the // object symbol_exprt s("foo", size_type()); byte_extract_exprt be = make_byte_extract(s, from_integer(0, c_index_type()), size_type()); - exprt simp = simplify_expr(be, ns); + exprt simp = simplify_expr(be, empty_namespace); REQUIRE(simp == s); } TEST_CASE("expr2bits and bits2expr respect bit order", "[core][util]") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); @@ -122,8 +116,7 @@ TEST_CASE("Simplify extractbit", "[core][util]") const cmdlinet cmdline; config.set(cmdline); - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); + auto &ns = empty_namespace; // binary: 1101 1110 1010 1101 1011 1110 1110 1111 // ^MSB LSB^ @@ -152,13 +145,10 @@ TEST_CASE("Simplify extractbits", "[core][util]") const cmdlinet cmdline; config.set(cmdline); - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); - const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); exprt eb = extractbits_exprt(deadbeef, 8, unsignedbv_typet(8)); - bool unmodified = simplify(eb, ns); + bool unmodified = simplify(eb, empty_namespace); REQUIRE(!unmodified); REQUIRE(eb == from_integer(0xbe, unsignedbv_typet(8))); @@ -166,8 +156,7 @@ TEST_CASE("Simplify extractbits", "[core][util]") TEST_CASE("Simplify shift", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); + auto &ns = empty_namespace; REQUIRE( simplify_expr(shl_exprt(from_integer(5, signedbv_typet(8)), 1), ns) == @@ -192,8 +181,7 @@ TEST_CASE("Simplify shift", "[core][util]") TEST_CASE("Simplify dynamic object comparison", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); + auto &ns = empty_namespace; dynamic_object_exprt dynamic_object(signedbv_typet(8)); dynamic_object.set_instance(1); @@ -238,23 +226,19 @@ TEST_CASE("Simplify pointer_object equality", "[core][util]") const cmdlinet cmdline; config.set(cmdline); - symbol_tablet symbol_table; - namespacet ns(symbol_table); - exprt p_o_void = pointer_object(null_pointer_exprt{pointer_type(empty_typet{})}); exprt p_o_int = pointer_object(null_pointer_exprt{pointer_type(signedbv_typet(32))}); - exprt simp = simplify_expr(equal_exprt{p_o_void, p_o_int}, ns); + exprt simp = simplify_expr(equal_exprt{p_o_void, p_o_int}, empty_namespace); REQUIRE(simp == true); } TEST_CASE("Simplify cast from bool", "[core][util]") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; { // this checks that ((int)B)==1 turns into B @@ -307,8 +291,7 @@ TEST_CASE("Simplify cast from bool", "[core][util]") TEST_CASE("simplify_expr boolean expressions", "[core][util]") { - symbol_tablet symbol_table; - namespacet ns{symbol_table}; + auto &ns = empty_namespace; SECTION("Binary boolean operations") { @@ -520,23 +503,19 @@ TEST_CASE("Simplifying cast expressions", "[core][util]") TEST_CASE("Simplify bitor", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); - SECTION("Simplification for raw bitvector") { bv_typet bv{4}; constant_exprt zero = from_integer(0, bv); symbol_exprt b{"B", bv}; - REQUIRE(simplify_expr(bitor_exprt{b, zero}, ns) == b); + REQUIRE(simplify_expr(bitor_exprt{b, zero}, empty_namespace) == b); } } TEST_CASE("Simplify inequality", "[core][util]") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; { // This checks that 3 < (B ? 4 : 5) simplifies to true, just like (B ? 4 : @@ -561,30 +540,27 @@ TEST_CASE("Simplify bitxor", "[core][util]") { config.set_arch("none"); - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); - SECTION("Simplification for c_bool") { constant_exprt false_c_bool = from_integer(0, c_bool_type()); REQUIRE( - simplify_expr(bitxor_exprt{false_c_bool, false_c_bool}, ns) == + simplify_expr( + bitxor_exprt{false_c_bool, false_c_bool}, empty_namespace) == false_c_bool); } } TEST_CASE("Simplify power", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - SECTION("Simplification for power") { symbol_exprt a{"a", integer_typet{}}; REQUIRE( - simplify_expr(power_exprt{a, from_integer(1, integer_typet{})}, ns) == a); + simplify_expr( + power_exprt{a, from_integer(1, integer_typet{})}, empty_namespace) == + a); } } @@ -592,8 +568,7 @@ TEST_CASE("Simplify pointer cast of pointer arithmetic", "[core][util]") { config.set_arch("none"); - symbol_tablet symbol_table; - namespacet ns(symbol_table); + auto &ns = empty_namespace; SECTION("Same element size: (char*)(unsigned_char_ptr + 1)") { @@ -632,8 +607,7 @@ TEST_CASE("Simplify pointer cast of pointer arithmetic", "[core][util]") TEST_CASE("Simplify quantifier", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; + auto &ns = empty_namespace; SECTION("Simplification for exists") { @@ -656,57 +630,42 @@ TEST_CASE("Simplify quantifier", "[core][util]") TEST_CASE("Simplify all-zero constant in bitand", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - const unsignedbv_typet u8{8}; const symbol_exprt x{"x", u8}; const auto zero = from_integer(0, u8); const bitand_exprt band{x, zero}; - REQUIRE(simplify_expr(band, ns) == zero); + REQUIRE(simplify_expr(band, empty_namespace) == zero); } TEST_CASE("Simplify all-ones constant in bitor", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - const unsignedbv_typet u8{8}; const symbol_exprt x{"x", u8}; const auto ones = from_integer(255, u8); const bitor_exprt bor{x, ones}; - REQUIRE(simplify_expr(bor, ns) == ones); + REQUIRE(simplify_expr(bor, empty_namespace) == ones); } TEST_CASE("Simplify all-zero constant in bitand with bv_typet", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - const bv_typet bv8{8}; const symbol_exprt x{"x", bv8}; const auto zero = bv8.all_zeros_expr(); const bitand_exprt band{x, zero}; - REQUIRE(simplify_expr(band, ns) == zero); + REQUIRE(simplify_expr(band, empty_namespace) == zero); } TEST_CASE("Simplify all-ones constant in bitor with bv_typet", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - const bv_typet bv8{8}; const symbol_exprt x{"x", bv8}; const auto ones = bv8.all_ones_expr(); const bitor_exprt bor{x, ones}; - REQUIRE(simplify_expr(bor, ns) == ones); + REQUIRE(simplify_expr(bor, empty_namespace) == ones); } TEST_CASE("Simplify flatten nested OR", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - const symbol_exprt a{"a", bool_typet{}}; const symbol_exprt b{"b", bool_typet{}}; const symbol_exprt c{"c", bool_typet{}}; @@ -714,14 +673,11 @@ TEST_CASE("Simplify flatten nested OR", "[core][util]") // (a || (b || c)) should flatten to (a || b || c) const or_exprt inner{b, c}; const or_exprt nested{a, inner}; - REQUIRE(simplify_expr(nested, ns) == or_exprt{a, b, c}); + REQUIRE(simplify_expr(nested, empty_namespace) == or_exprt{a, b, c}); } TEST_CASE("Simplify flatten nested AND", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - const symbol_exprt a{"a", bool_typet{}}; const symbol_exprt b{"b", bool_typet{}}; const symbol_exprt c{"c", bool_typet{}}; @@ -729,43 +685,34 @@ TEST_CASE("Simplify flatten nested AND", "[core][util]") // (a && (b && c)) should flatten to (a && b && c) const and_exprt inner{b, c}; const and_exprt nested{a, inner}; - REQUIRE(simplify_expr(nested, ns) == and_exprt{a, b, c}); + REQUIRE(simplify_expr(nested, empty_namespace) == and_exprt{a, b, c}); } TEST_CASE("Simplify complementary pair in OR", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - const symbol_exprt a{"a", bool_typet{}}; // (a || !a) should simplify to true const or_exprt expr{a, not_exprt{a}}; - REQUIRE(simplify_expr(expr, ns) == true_exprt{}); + REQUIRE(simplify_expr(expr, empty_namespace) == true_exprt{}); } TEST_CASE("Simplify complementary pair in AND", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - const symbol_exprt a{"a", bool_typet{}}; // (a && !a) should simplify to false const and_exprt expr{a, not_exprt{a}}; - REQUIRE(simplify_expr(expr, ns) == false_exprt{}); + REQUIRE(simplify_expr(expr, empty_namespace) == false_exprt{}); } TEST_CASE("Simplify complementary pair in nested OR", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - const symbol_exprt a{"a", bool_typet{}}; const symbol_exprt b{"b", bool_typet{}}; // (a || (b || !a)) should simplify to true (after flattening) const or_exprt inner{b, not_exprt{a}}; const or_exprt expr{a, inner}; - REQUIRE(simplify_expr(expr, ns) == true_exprt{}); + REQUIRE(simplify_expr(expr, empty_namespace) == true_exprt{}); } diff --git a/unit/util/std_expr.cpp b/unit/util/std_expr.cpp index b21425164c9..1a5052e8c5e 100644 --- a/unit/util/std_expr.cpp +++ b/unit/util/std_expr.cpp @@ -6,8 +6,6 @@ Author: Diffblue Ltd \*******************************************************************/ -#include - #include #include #include @@ -16,7 +14,9 @@ Author: Diffblue Ltd #include #include #include -#include + +#include +#include TEST_CASE("for a division expression...", "[unit][util][std_expr]") { @@ -40,8 +40,7 @@ TEST_CASE("object descriptor expression", "[unit][util][std_expr]") { config.ansi_c.set_LP64(); - symbol_tablet symbol_table; - const namespacet ns(symbol_table); + const auto &ns = empty_namespace; array_typet array_type(signed_int_type(), from_integer(2, size_type())); struct_typet struct_type({{"foo", array_type}}); From 16119b01912bc7a5b4d035b53171a0f0b3aa6181 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 25 May 2026 20:00:35 +0000 Subject: [PATCH 4/6] Drop unused includes in tests migrated to empty_namespacet Eight unit tests had a 'symbol_tablet symbol_table; namespacet ns(symbol_table);' pair that was declared but never used. The preceding commit removed those declarations as part of the migration to empty_namespacet, but left both '#include ' and the newly-added '#include ' in place. Neither header is referenced from these files: there is no mention of 'namespacet' nor of 'empty_namespace' anywhere in their bodies. Drop both includes from: - unit/util/interval/{add,comparisons,multiply,modulo,subtract}.cpp - unit/analyses/does_remove_const/{does_expr_lose_const, does_type_preserve_const_correctness, is_type_at_least_as_const_as}.cpp CODING_STANDARD.md asks to avoid unnecessary includes. Co-authored-by: Kiro --- unit/analyses/does_remove_const/does_expr_lose_const.cpp | 2 -- .../does_remove_const/does_type_preserve_const_correctness.cpp | 2 -- .../analyses/does_remove_const/is_type_at_least_as_const_as.cpp | 2 -- unit/util/interval/add.cpp | 2 -- unit/util/interval/comparisons.cpp | 2 -- unit/util/interval/modulo.cpp | 2 -- unit/util/interval/multiply.cpp | 2 -- unit/util/interval/subtract.cpp | 2 -- 8 files changed, 16 deletions(-) diff --git a/unit/analyses/does_remove_const/does_expr_lose_const.cpp b/unit/analyses/does_remove_const/does_expr_lose_const.cpp index 7b700922d3b..c1e399b54c7 100644 --- a/unit/analyses/does_remove_const/does_expr_lose_const.cpp +++ b/unit/analyses/does_remove_const/does_expr_lose_const.cpp @@ -11,7 +11,6 @@ Author: Diffblue Ltd. #include #include -#include #include #include @@ -20,7 +19,6 @@ Author: Diffblue Ltd. #include #include #include -#include #include SCENARIO("does_expr_lose_const", diff --git a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp index 450c561346c..98f3ea25b52 100644 --- a/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp +++ b/unit/analyses/does_remove_const/does_type_preserve_const_correctness.cpp @@ -11,14 +11,12 @@ Author: Diffblue Ltd. #include #include -#include #include #include #include #include -#include #include SCENARIO("does_type_preserve_const_correctness", diff --git a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp index 7b9de00d26f..a7fa63e5e13 100644 --- a/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp +++ b/unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp @@ -11,14 +11,12 @@ Author: Diffblue Ltd. #include #include -#include #include #include #include #include -#include #include SCENARIO("is_type_at_least_as_const", diff --git a/unit/util/interval/add.cpp b/unit/util/interval/add.cpp index a7d6dd8e916..5119fea0fb3 100644 --- a/unit/util/interval/add.cpp +++ b/unit/util/interval/add.cpp @@ -6,9 +6,7 @@ #include #include #include -#include -#include #include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) diff --git a/unit/util/interval/comparisons.cpp b/unit/util/interval/comparisons.cpp index 9402df62e95..d37a24c3d07 100644 --- a/unit/util/interval/comparisons.cpp +++ b/unit/util/interval/comparisons.cpp @@ -6,9 +6,7 @@ #include #include #include -#include -#include #include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) diff --git a/unit/util/interval/modulo.cpp b/unit/util/interval/modulo.cpp index 4872961740c..972d4fdb55f 100644 --- a/unit/util/interval/modulo.cpp +++ b/unit/util/interval/modulo.cpp @@ -6,9 +6,7 @@ #include #include #include -#include -#include #include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) diff --git a/unit/util/interval/multiply.cpp b/unit/util/interval/multiply.cpp index 48fdcbd3030..92272aeeeaf 100644 --- a/unit/util/interval/multiply.cpp +++ b/unit/util/interval/multiply.cpp @@ -6,9 +6,7 @@ #include #include #include -#include -#include #include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) diff --git a/unit/util/interval/subtract.cpp b/unit/util/interval/subtract.cpp index 8790c25fd3e..7240abe6e66 100644 --- a/unit/util/interval/subtract.cpp +++ b/unit/util/interval/subtract.cpp @@ -6,9 +6,7 @@ #include #include #include -#include -#include #include #define V(X) (bvrep2integer(X.get(ID_value).c_str(), 32, true)) From 03db5c5c232d1549a63647a6790edaa30c5b54d2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 25 May 2026 20:05:31 +0000 Subject: [PATCH 5/6] Add smoke test for empty_namespacet Add a smoke test that exercises empty_namespacet through a const namespacet & reference: an absent symbol lookup returns true and leaves the out-parameter null, and smallest_unused_suffix returns 0 for any prefix. The test documents the helper's contract and acts as a regression test if anyone ever changes the inheritance order or the base-from-member cast in empty_namespacet's constructor. Following the convention established by unit/get_goto_model_from_c_test.cpp, the new file lives at the top of unit/ rather than inside unit/testing-utils/: anything matched by testing-utils/*.cpp is removed from the unit executable's sources by unit/CMakeLists.txt and built into the testing-utils library instead, so a TEST_CASE placed there would never run. Also tighten the empty_namespacet constructor to use a reference static_cast (static_cast(*this)) rather than a pointer cast and dereference, which is slightly more idiomatic when the cast target is a base subobject. Co-authored-by: Kiro --- unit/Makefile | 1 + unit/empty_namespace_test.cpp | 30 ++++++++++++++++++++++++++++ unit/testing-utils/empty_namespace.h | 2 +- 3 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 unit/empty_namespace_test.cpp diff --git a/unit/Makefile b/unit/Makefile index fa46a11d30c..0f5bec6ec27 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -54,6 +54,7 @@ SRC += analyses/ai/ai.cpp \ ansi-c/c_typecheck_base.cpp \ big-int/big-int.cpp \ compound_block_locations.cpp \ + empty_namespace_test.cpp \ get_goto_model_from_c_test.cpp \ goto-cc/armcc_cmdline.cpp \ goto-checker/properties/property_status.cpp \ diff --git a/unit/empty_namespace_test.cpp b/unit/empty_namespace_test.cpp new file mode 100644 index 00000000000..33f48a6db4f --- /dev/null +++ b/unit/empty_namespace_test.cpp @@ -0,0 +1,30 @@ +/*******************************************************************\ + +Module: Smoke test for empty_namespacet + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Verify that the empty_namespace global is a usable +/// const namespacet & whose symbol table is empty. The test exists to +/// document the contract and to act as a regression test if anyone ever +/// changes the inheritance order or the base-from-member cast in +/// empty_namespacet's constructor. + +#include +#include + +TEST_CASE( + "empty_namespace is a usable empty namespacet", + "[core][testing-utils]") +{ + const namespacet &ns = empty_namespace; + + const symbolt *symbol = nullptr; + REQUIRE(ns.lookup("does_not_exist", symbol)); + REQUIRE(symbol == nullptr); + + REQUIRE(ns.smallest_unused_suffix("x") == 0); +} diff --git a/unit/testing-utils/empty_namespace.h b/unit/testing-utils/empty_namespace.h index b06438701ab..b5d156ccda1 100644 --- a/unit/testing-utils/empty_namespace.h +++ b/unit/testing-utils/empty_namespace.h @@ -22,7 +22,7 @@ Author: Michael Tautschnig class empty_namespacet : private symbol_tablet, public namespacet { public: - empty_namespacet() : namespacet{*static_cast(this)} + empty_namespacet() : namespacet{static_cast(*this)} { } From 5645a216bbf1a65b5b00cf00fb8ed8fe7c1c6825 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 25 May 2026 20:10:51 +0000 Subject: [PATCH 6/6] Prefer empty_namespace inline or const namespacet & alias After the migration to empty_namespacet, around 50 unit tests had declared a 'auto &ns = empty_namespace;' (or 'const auto &') alias. Two issues with the auto& form: 1. The deduced type is the implementation class 'const empty_namespacet &' rather than the abstract 'const namespacet &', so test code is unnecessarily coupled to the helper's class. 2. At sites where the alias was used only once or twice, the alias declaration was longer than the inline form would have been. Sweep these sites, applying a per-scope rule: * If 'ns' is referenced no more than twice within the surrounding brace scope, drop the alias and use 'empty_namespace' inline. * Otherwise keep the alias but make the type explicit: 'const namespacet &ns = empty_namespace;'. The choice is stylistic; the test bodies are unchanged. All 538 unit test cases / 19053 assertions still pass. Co-authored-by: Kiro --- unit/analyses/ai/ai_simplify_lhs.cpp | 2 +- .../abstract_environment/to_predicate.cpp | 2 +- .../abstract_object/index_range.cpp | 6 +-- .../abstract_object/merge.cpp | 5 +-- .../constant_abstract_value/meet.cpp | 2 +- .../constant_abstract_value/merge.cpp | 2 +- .../constant_abstract_value/to_predicate.cpp | 6 +-- .../to_predicate.cpp | 3 +- .../eval-member-access.cpp | 2 +- .../maximum_length.cpp | 2 +- .../full_array_abstract_object/merge.cpp | 2 +- .../to_predicate.cpp | 2 +- .../full_struct_abstract_object/merge.cpp | 2 +- .../to_predicate.cpp | 2 +- .../extremes-go-top.cpp | 2 +- .../interval_abstract_value/meet.cpp | 2 +- .../interval_abstract_value/merge.cpp | 2 +- .../interval_abstract_value/to_predicate.cpp | 5 +-- .../widening_merge.cpp | 2 +- .../value_expression_evaluation/assume.cpp | 2 +- .../assume_prune.cpp | 2 +- .../expression_evaluation.cpp | 2 +- .../value_set_abstract_object/compacting.cpp | 2 +- .../extremes-go-top.cpp | 2 +- .../value_set_abstract_object/meet.cpp | 2 +- .../value_set_abstract_object/merge.cpp | 2 +- .../to_predicate.cpp | 2 +- .../widening_merge.cpp | 2 +- .../to_predicate.cpp | 2 +- .../to_predicate.cpp | 2 +- unit/goto-programs/goto_trace_output.cpp | 3 +- unit/goto-programs/xml_expr.cpp | 6 +-- unit/goto-symex/is_constant.cpp | 4 +- unit/solvers/bdd/miniBDD/miniBDD.cpp | 15 +++----- unit/solvers/flattening/boolbv.cpp | 3 +- .../solvers/flattening/boolbv_enumeration.cpp | 3 +- unit/solvers/flattening/boolbv_onehot.cpp | 3 +- unit/solvers/flattening/boolbv_update_bit.cpp | 3 +- .../smt2_incremental/convert_expr_to_smt.cpp | 37 +++++++++---------- .../get_numeric_value_from_character.cpp | 3 +- .../is_digit_with_radix.cpp | 3 +- .../length_for_format_specifier.cpp | 2 +- .../length_of_decimal_int.cpp | 9 ++--- .../string_refinement/string_refinement.cpp | 3 +- unit/util/bitvector_expr.cpp | 3 +- unit/util/interval/get_extreme.cpp | 2 +- unit/util/lower_byte_operators.cpp | 6 +-- unit/util/pointer_offset_size.cpp | 4 +- unit/util/simplify_expr.cpp | 30 ++++++--------- unit/util/std_expr.cpp | 2 +- 50 files changed, 94 insertions(+), 125 deletions(-) diff --git a/unit/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index 8384f46c4c4..96e6b0cd735 100644 --- a/unit/analyses/ai/ai_simplify_lhs.cpp +++ b/unit/analyses/ai/ai_simplify_lhs.cpp @@ -71,7 +71,7 @@ SCENARIO("ai_domain_baset::ai_simplify_lhs", { ansi_c_languaget language; - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; constant_simplification_mockt mock_ai_domain; diff --git a/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp b/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp index ef9257e6fa0..c5b3f7a4ef6 100644 --- a/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp @@ -28,7 +28,7 @@ SCENARIO( config.context_tracking.last_write_context = false; auto object_factory = variable_sensitivity_object_factoryt::configured_with(config); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("an abstract environment") { diff --git a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp index 4e5f44b26b2..424da3c94b9 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/index_range.cpp @@ -30,7 +30,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt env{object_factory}; env.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("an integer constant has an index_range") { @@ -94,7 +94,7 @@ SCENARIO( vsd_configt::intervals()); abstract_environmentt env{object_factory}; env.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; auto type = signedbv_typet(32); GIVEN("a top intervals's range is empty") @@ -194,7 +194,7 @@ SCENARIO( vsd_configt::intervals()); abstract_environmentt env{object_factory}; env.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; auto type = signedbv_typet(32); GIVEN("a TOP value_set is empty") diff --git a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp index 2fc2be468c2..88f57b3482a 100644 --- a/unit/analyses/variable-sensitivity/abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/abstract_object/merge.cpp @@ -93,12 +93,11 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; WHEN("merging TOP with 1") { auto top1 = make_top_object(); - auto op2 = make_constant(val1, environment, ns); + auto op2 = make_constant(val1, environment, empty_namespace); auto result = abstract_objectt::merge(top1, op2, widen_modet::no); @@ -137,7 +136,7 @@ SCENARIO( WHEN("merging BOTTOM with 1") { auto op1 = make_bottom_object(); - auto op2 = make_constant(val1, environment, ns); + auto op2 = make_constant(val1, environment, empty_namespace); auto result = abstract_objectt::merge(op1, op2, widen_modet::no); diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp index 0ee4a750052..eed4e4ef71e 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/meet.cpp @@ -74,7 +74,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("meeting two constants") { diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp index 7e9833ae6f1..17099429e22 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/merge.cpp @@ -48,7 +48,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("merging two constants") { diff --git a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp index 0b280e17976..d82c5fbaa67 100644 --- a/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp @@ -34,7 +34,6 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; GIVEN("constant_abstract_value") { @@ -50,13 +49,14 @@ SCENARIO( } WHEN("x = 2") { - auto obj = make_constant(val2, environment, ns); + auto obj = make_constant(val2, environment, empty_namespace); THEN_PREDICATE(obj, "x == 2"); } WHEN("(1 + 2) = 3") { auto val1 = from_integer(1, type); - auto c3 = make_constant(from_integer(3, type), environment, ns); + auto c3 = + make_constant(from_integer(3, type), environment, empty_namespace); auto pred = c3->to_predicate(plus_exprt(val1, val2)); THEN("predicate is (1 + 2) = 3") diff --git a/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp index d8441ca2196..49419ca540e 100644 --- a/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp @@ -35,7 +35,6 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; GIVEN("constant_pointer_abstract_object") { @@ -55,7 +54,7 @@ SCENARIO( { const auto address_of = address_of_exprt(val2_symbol); auto obj = std::make_shared( - address_of, environment, ns); + address_of, environment, empty_namespace); THEN_PREDICATE(obj, "x == &val2"); } } diff --git a/unit/analyses/variable-sensitivity/eval-member-access.cpp b/unit/analyses/variable-sensitivity/eval-member-access.cpp index 891300199b2..dceb954181b 100644 --- a/unit/analyses/variable-sensitivity/eval-member-access.cpp +++ b/unit/analyses/variable-sensitivity/eval-member-access.cpp @@ -33,7 +33,7 @@ SCENARIO( vsd_configt::constant_domain())}; environment.make_top(); // Domains are bottom on construction - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("An array of {1, 2, 3}") { diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp index 4ff546de306..2ffa3e45ca2 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp @@ -52,7 +52,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(configuration); abstract_environmentt environment(object_factory); environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; WHEN("maximum size is " + std::to_string(max_array_index)) { WHEN("array = {1, 2, 3}, writes under maximum size") diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp index e42d3bae669..420cc7b1634 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp @@ -47,7 +47,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt environment(object_factory); environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; WHEN("Merging two constant array AOs with the same array") { diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp index 55759c6509e..e0b493be628 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp @@ -22,7 +22,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt environment(object_factory); environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("full_array_abstract_object to predicate") { diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp index 48f069f702c..88f27cbbe14 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp @@ -45,7 +45,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt environment(object_factory); environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; WHEN("Merging two constant struct AOs with the same contents") { diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp index 3cee65819c9..e2d3aac03bc 100644 --- a/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/full_struct_abstract_object/to_predicate.cpp @@ -22,7 +22,7 @@ SCENARIO( vsd_configt::constant_domain()); abstract_environmentt environment(object_factory); environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("full_struct_abstract_object to predicate") { diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp index abbcfa20de3..05cdd081e93 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp @@ -38,7 +38,7 @@ SCENARIO( auto environment = abstract_environmentt{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("[min-max] signed goes TOP") { diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp index 84cd99c8491..c00b94ff09c 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/meet.cpp @@ -86,7 +86,7 @@ SCENARIO( abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("meeting two intervals") { diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp index f6ec64cc24b..42802d98f10 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp @@ -52,7 +52,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("merging two intervals") { diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp index 8fb084be827..cdce7f95f6c 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp @@ -44,7 +44,6 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; GIVEN("interval_abstract_value") { @@ -60,12 +59,12 @@ SCENARIO( } WHEN("[ 2 ]") { - auto obj = make_interval(val2, val2, environment, ns); + auto obj = make_interval(val2, val2, environment, empty_namespace); THEN_PREDICATE(obj, "x == 2"); } WHEN("[ 0, 2 ]") { - auto obj = make_interval(val0, val2, environment, ns); + auto obj = make_interval(val0, val2, environment, empty_namespace); THEN_PREDICATE(obj, "0 <= x && x <= 2"); } } diff --git a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp index fbd89178eea..438b18fbbb6 100644 --- a/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp @@ -60,7 +60,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("interval merges which don't widen") { diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp index a6745ae9d9b..bf0786ee569 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp @@ -170,7 +170,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; assume_testert assumeTester(environment, ns); diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp index 1f41f8f1856..0600cfd31ba 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp @@ -81,7 +81,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; auto type = signedbv_typet(32); auto val0 = from_integer(0, type); diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp index 355a1f32ab5..75b5f081630 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp @@ -44,7 +44,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("adding two constants") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp index 170dbabf9cd..2af278484e9 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp @@ -51,7 +51,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); auto environment = abstract_environmentt{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("compact values into existing interval") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp index c1a99fef46e..a65188bef00 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/extremes-go-top.cpp @@ -27,7 +27,7 @@ SCENARIO( auto environment = abstract_environmentt{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("{FALSE, TRUE} goes TOP") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp index 4495e6bb77a..58730924665 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/meet.cpp @@ -76,7 +76,7 @@ SCENARIO( abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("meeting two value_sets") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp index 1fd4edd60f2..c2513b7452a 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/merge.cpp @@ -49,7 +49,7 @@ SCENARIO( vsd_configt::value_set()); auto environment = abstract_environmentt{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("merging two value sets") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp index f612e5496cd..4b6b5775e3a 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp @@ -46,7 +46,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("value_set_abstract_object") { diff --git a/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp index 9ecc59a2e82..e5808de6ac0 100644 --- a/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp +++ b/unit/analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp @@ -68,7 +68,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("value_set merges which don't widen") { diff --git a/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp index 6ba46fb0f4f..531a815eb02 100644 --- a/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp @@ -44,7 +44,7 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("value_set_pointer_abstract_object") { diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp index fc16bce44e4..b5dec0c7563 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp @@ -26,7 +26,7 @@ SCENARIO( config.context_tracking.last_write_context = false; auto object_factory = variable_sensitivity_object_factoryt::configured_with(config); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("to_predicate()") { diff --git a/unit/goto-programs/goto_trace_output.cpp b/unit/goto-programs/goto_trace_output.cpp index e6b6045caab..28b7d6f1c16 100644 --- a/unit/goto-programs/goto_trace_output.cpp +++ b/unit/goto-programs/goto_trace_output.cpp @@ -20,7 +20,6 @@ SCENARIO( "Output trace with nil lhs object", "[core][goto-programs][goto_trace]") { - auto &ns = empty_namespace; goto_programt::instructionst instructions; instructions.emplace_back(goto_program_instruction_typet::OTHER); goto_trace_stept step; @@ -28,7 +27,7 @@ SCENARIO( step.type = goto_trace_stept::typet::ATOMIC_BEGIN; std::ostringstream oss; - step.output(ns, oss); + step.output(empty_namespace, oss); std::istringstream iss(oss.str()); std::string line; diff --git a/unit/goto-programs/xml_expr.cpp b/unit/goto-programs/xml_expr.cpp index 20971950bc9..0bd4a1af12e 100644 --- a/unit/goto-programs/xml_expr.cpp +++ b/unit/goto-programs/xml_expr.cpp @@ -20,10 +20,8 @@ TEST_CASE("Constant expression to XML") { config.set_arch("none"); - const auto &ns = empty_namespace; - const constant_exprt number_ubv = from_integer(0xFF, unsignedbv_typet(8)); - const xmlt x_ubv = xml(number_ubv, ns); + const xmlt x_ubv = xml(number_ubv, empty_namespace); REQUIRE(x_ubv.get_attribute("binary") == "11111111"); @@ -32,7 +30,7 @@ TEST_CASE("Constant expression to XML") fixedbv_type.set_integer_bits(6); const constant_exprt number_fbv = from_integer(0x3, fixedbv_type); - const xmlt x_fbv = xml(number_fbv, ns); + const xmlt x_fbv = xml(number_fbv, empty_namespace); REQUIRE(x_fbv.get_attribute("binary") == "00001100"); } diff --git a/unit/goto-symex/is_constant.cpp b/unit/goto-symex/is_constant.cpp index e606354ed55..27c441b9b43 100644 --- a/unit/goto-symex/is_constant.cpp +++ b/unit/goto-symex/is_constant.cpp @@ -16,14 +16,12 @@ Author: Diffblue Ltd. SCENARIO("goto-symex-is-constant", "[core][goto-symex][is_constant]") { - auto &ns = empty_namespace; - signedbv_typet int_type(32); constant_exprt sizeof_constant("4", int_type); sizeof_constant.set(ID_C_c_sizeof_type, int_type); symbol_exprt non_constant("x", int_type); - goto_symex_can_forward_propagatet is_constant(ns); + goto_symex_can_forward_propagatet is_constant(empty_namespace); GIVEN("Sizeof expression multiplied by a non-constant") { diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp index f5da98eee69..ee40fff6a6e 100644 --- a/unit/solvers/bdd/miniBDD/miniBDD.cpp +++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp @@ -201,10 +201,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x&!x==0") { - auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); - boolbvt boolbv(ns, bdd_prop, null_message_handler); + boolbvt boolbv(empty_namespace, bdd_prop, null_message_handler); unsignedbv_typet type(2); symbol_exprt var("x", type); @@ -218,10 +217,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x+x==1") { - auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); - boolbvt boolbv(ns, bdd_prop, null_message_handler); + boolbvt boolbv(empty_namespace, bdd_prop, null_message_handler); unsignedbv_typet type(32); symbol_exprt var("x", type); @@ -234,10 +232,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*y==y*x") { - auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); - boolbvt boolbv(ns, bdd_prop, null_message_handler); + boolbvt boolbv(empty_namespace, bdd_prop, null_message_handler); unsignedbv_typet type(4); symbol_exprt var_x("x", type); @@ -251,10 +248,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*x==2") { - auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); - boolbvt boolbv(ns, bdd_prop, null_message_handler); + boolbvt boolbv(empty_namespace, bdd_prop, null_message_handler); unsignedbv_typet type(8); symbol_exprt var_x("x", type); @@ -267,10 +263,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*x==4") { - auto &ns = empty_namespace; mini_bdd_mgrt bdd_mgr; bdd_propt bdd_prop(bdd_mgr); - boolbvt boolbv(ns, bdd_prop, null_message_handler); + boolbvt boolbv(empty_namespace, bdd_prop, null_message_handler); unsignedbv_typet type(8); symbol_exprt var_x("x", type); diff --git a/unit/solvers/flattening/boolbv.cpp b/unit/solvers/flattening/boolbv.cpp index 1ef4e6d31dd..9f0bde9234a 100644 --- a/unit/solvers/flattening/boolbv.cpp +++ b/unit/solvers/flattening/boolbv.cpp @@ -28,8 +28,7 @@ SCENARIO("boolbvt", "[core][solvers][flattening][boolbvt]") GIVEN("A satisfiable bit-vector formula f") { satcheckt satcheck(message_handler); - auto &ns = empty_namespace; - boolbvt boolbv(ns, satcheck, message_handler); + boolbvt boolbv(empty_namespace, satcheck, message_handler); unsignedbv_typet u32(32); boolbv << equal_exprt(symbol_exprt("x", u32), from_integer(10, u32)); diff --git a/unit/solvers/flattening/boolbv_enumeration.cpp b/unit/solvers/flattening/boolbv_enumeration.cpp index 6571ceea591..484db42896c 100644 --- a/unit/solvers/flattening/boolbv_enumeration.cpp +++ b/unit/solvers/flattening/boolbv_enumeration.cpp @@ -23,8 +23,7 @@ TEST_CASE( console_message_handlert message_handler; message_handler.set_verbosity(0); satcheckt satcheck{message_handler}; - auto &ns = empty_namespace; - boolbvt boolbv{ns, satcheck, message_handler}; + boolbvt boolbv{empty_namespace, satcheck, message_handler}; enumeration_typet enumeration; enumeration.elements().push_back(irept{"A"}); enumeration.elements().push_back(irept{"B"}); diff --git a/unit/solvers/flattening/boolbv_onehot.cpp b/unit/solvers/flattening/boolbv_onehot.cpp index 9ac154ffc65..509652dfe39 100644 --- a/unit/solvers/flattening/boolbv_onehot.cpp +++ b/unit/solvers/flattening/boolbv_onehot.cpp @@ -25,8 +25,7 @@ TEST_CASE("onehot flattening", "[core][solvers][flattening][boolbvt][onehot]") console_message_handlert message_handler; message_handler.set_verbosity(0); satcheckt satcheck{message_handler}; - auto &ns = empty_namespace; - boolbvt boolbv{ns, satcheck, message_handler}; + boolbvt boolbv{empty_namespace, satcheck, message_handler}; unsignedbv_typet u8{8}; GIVEN("A bit-vector that is one-hot") diff --git a/unit/solvers/flattening/boolbv_update_bit.cpp b/unit/solvers/flattening/boolbv_update_bit.cpp index 92530c78e4a..3fbc8bca877 100644 --- a/unit/solvers/flattening/boolbv_update_bit.cpp +++ b/unit/solvers/flattening/boolbv_update_bit.cpp @@ -31,8 +31,7 @@ SCENARIO( GIVEN("A satisfiable bit-vector formula f with update_bit") { satcheckt satcheck{message_handler}; - auto &ns = empty_namespace; - boolbvt boolbv{ns, satcheck, message_handler}; + boolbvt boolbv{empty_namespace, satcheck, message_handler}; unsignedbv_typet u32{32}; boolbv << equal_exprt( diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 49b1cbcefe0..aea2daf2762 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -469,11 +469,11 @@ TEST_CASE( { // (int32_t *)a + 2 const auto pointer_arith_expr = plus_exprt{pointer_a, two_bvint_32bit}; - const auto &ns = empty_namespace; - track_expression_objects(pointer_arith_expr, ns, test.object_map); + track_expression_objects( + pointer_arith_expr, empty_namespace, test.object_map); associate_pointer_sizes( pointer_arith_expr, - ns, + empty_namespace, test.pointer_sizes, test.object_map, test.object_size_function.make_application, @@ -544,11 +544,11 @@ TEST_CASE( // (int *)a - 2 is coming to us as (int *)a + (-2), so a design decision // was made to handle only that form. const auto pointer_arith_expr = plus_exprt{pointer_a, minus_two_bvint}; - const auto &ns = empty_namespace; - track_expression_objects(pointer_arith_expr, ns, test.object_map); + track_expression_objects( + pointer_arith_expr, empty_namespace, test.object_map); associate_pointer_sizes( pointer_arith_expr, - ns, + empty_namespace, test.pointer_sizes, test.object_map, test.object_size_function.make_application, @@ -575,11 +575,11 @@ TEST_CASE( const auto two_bvint = from_integer(2, signedbv_typet{pointer_width}); const auto pointer_arith_expr = minus_exprt{pointer_a, two_bvint}; - const auto &ns = empty_namespace; - track_expression_objects(pointer_arith_expr, ns, test.object_map); + track_expression_objects( + pointer_arith_expr, empty_namespace, test.object_map); associate_pointer_sizes( pointer_arith_expr, - ns, + empty_namespace, test.pointer_sizes, test.object_map, test.object_size_function.make_application, @@ -612,11 +612,11 @@ TEST_CASE( { // (int32_t *)a - (int32_t *)b const auto pointer_subtraction = minus_exprt{pointer_b, pointer_a}; - const auto &ns = empty_namespace; - track_expression_objects(pointer_subtraction, ns, test.object_map); + track_expression_objects( + pointer_subtraction, empty_namespace, test.object_map); associate_pointer_sizes( pointer_subtraction, - ns, + empty_namespace, test.pointer_sizes, test.object_map, test.object_size_function.make_application, @@ -1467,7 +1467,7 @@ TEST_CASE( { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64); - const auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; const symbol_exprt foo{"foo", unsignedbv_typet{32}}; const symbol_exprt bar{"bar", unsignedbv_typet{32}}; SECTION("Address of symbol") @@ -1669,11 +1669,10 @@ TEST_CASE( { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64); - const auto &ns = empty_namespace; const symbol_exprt foo{"foo", unsignedbv_typet{32}}; const object_size_exprt object_size{ address_of_exprt{foo}, unsignedbv_typet{64}}; - track_expression_objects(object_size, ns, test.object_map); + track_expression_objects(object_size, empty_namespace, test.object_map); const auto foo_id = 2; CHECK(test.object_map.at(foo).unique_id == foo_id); const auto object_bits = config.bv_encoding.object_bits; @@ -1693,10 +1692,9 @@ TEST_CASE( { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64); - const auto &ns = empty_namespace; const symbol_exprt foo{"foo", unsignedbv_typet{32}}; const is_dynamic_object_exprt is_dynamic_object{address_of_exprt{foo}}; - track_expression_objects(is_dynamic_object, ns, test.object_map); + track_expression_objects(is_dynamic_object, empty_namespace, test.object_map); const auto foo_id = 2; CHECK(test.object_map.at(foo).unique_id == foo_id); const auto object_bits = config.bv_encoding.object_bits; @@ -1716,7 +1714,6 @@ TEST_CASE( { auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64); - const auto &ns = empty_namespace; const typet value_type = signedbv_typet{8}; const exprt array = symbol_exprt{ "my_array", array_typet{value_type, from_integer(10, signed_size_type())}}; @@ -1748,10 +1745,10 @@ TEST_CASE( { const symbol_exprt symbol{"a_symbol", address_of_expr.type()}; const equal_exprt assignment{symbol, address_of_expr}; - track_expression_objects(assignment, ns, test.object_map); + track_expression_objects(assignment, empty_namespace, test.object_map); associate_pointer_sizes( assignment, - ns, + empty_namespace, test.pointer_sizes, test.object_map, test.object_size_function.make_application, diff --git a/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp b/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp index 0531ca3ed38..c2991a275e9 100644 --- a/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp +++ b/unit/solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp @@ -24,11 +24,10 @@ static exprt actual( const unsigned long radix_ul) { const constant_exprt chr = from_integer(character, char_type); - const auto &ns = empty_namespace; return simplify_expr( get_numeric_value_from_character( chr, char_type, int_type, strict_formatting, radix_ul), - ns); + empty_namespace); } SCENARIO( diff --git a/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp b/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp index 8feada5927d..a898e423cf2 100644 --- a/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp +++ b/unit/solvers/strings/string_constraint_generator_valueof/is_digit_with_radix.cpp @@ -23,12 +23,11 @@ static exprt actual( { const typet char_type = unsignedbv_typet(16); const constant_exprt chr = from_integer(int_value, char_type); - const auto &ns = empty_namespace; return simplify_expr( is_digit_with_radix( std::move(chr), strict_formatting, radix_as_char, radix_ul), - ns); + empty_namespace); } /// Get the simplified return value of is_digit_with_radix called with a radix diff --git a/unit/solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp b/unit/solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp index 30cb193952c..607a49d1350 100644 --- a/unit/solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp +++ b/unit/solvers/strings/string_format_builtin_function/length_for_format_specifier.cpp @@ -48,7 +48,7 @@ SCENARIO( const std::size_t pointer_width = 16; const auto pointer_type = pointer_typet(char_type, pointer_width); - const auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; symbol_generatort fresh_symbol; array_poolt array_pool{fresh_symbol}; diff --git a/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp b/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp index 3ab805dec4c..7c39d2caa09 100644 --- a/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp +++ b/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp @@ -19,8 +19,6 @@ SCENARIO( { const typet type = signedbv_typet(32); - const auto &ns = empty_namespace; - const std::vector input_values = { 0, 1, 10, 15, 999, 1000000001, -1, -21111111, -1234567890}; const std::vector oracles_for_base_10 = {1, 1, 2, 2, 3, 10, 2, 9, 11}; @@ -38,7 +36,8 @@ SCENARIO( THEN("length expression is " << oracle) { const int actual_int = - numeric_cast(to_constant_expr(simplify_expr(actual, ns))) + numeric_cast( + to_constant_expr(simplify_expr(actual, empty_namespace))) .value(); REQUIRE(actual_int == oracle); } @@ -57,8 +56,8 @@ SCENARIO( const int oracle = oracles_for_base_16[i]; THEN("length expression is " << oracle) { - const int actual_int = - *numeric_cast(to_constant_expr(simplify_expr(actual, ns))); + const int actual_int = *numeric_cast( + to_constant_expr(simplify_expr(actual, empty_namespace))); REQUIRE(actual_int == oracle); } } diff --git a/unit/solvers/strings/string_refinement/string_refinement.cpp b/unit/solvers/strings/string_refinement/string_refinement.cpp index e9353bcc9a9..468914e852c 100644 --- a/unit/solvers/strings/string_refinement/string_refinement.cpp +++ b/unit/solvers/strings/string_refinement/string_refinement.cpp @@ -27,8 +27,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]") null_message_handlert log{}; info.message_handler = &log; - auto &ns = empty_namespace; - info.ns = &ns; + info.ns = &empty_namespace; satcheckt sat_solver{log}; info.prop = &sat_solver; diff --git a/unit/util/bitvector_expr.cpp b/unit/util/bitvector_expr.cpp index 82aa4ee98cd..faac4794a7d 100644 --- a/unit/util/bitvector_expr.cpp +++ b/unit/util/bitvector_expr.cpp @@ -77,8 +77,7 @@ TEST_CASE("onehot expression lowering", "[core][util][expr]") console_message_handlert message_handler; message_handler.set_verbosity(0); satcheckt satcheck{message_handler}; - auto &ns = empty_namespace; - boolbvt boolbv{ns, satcheck, message_handler}; + boolbvt boolbv{empty_namespace, satcheck, message_handler}; unsignedbv_typet u8{8}; GIVEN("A bit-vector that is one-hot") diff --git a/unit/util/interval/get_extreme.cpp b/unit/util/interval/get_extreme.cpp index 5d772530b8b..5d5a3609ed9 100644 --- a/unit/util/interval/get_extreme.cpp +++ b/unit/util/interval/get_extreme.cpp @@ -23,7 +23,7 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]") { GIVEN("A selection of constant_exprts in a std::vector and map") { - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; std::vector ve; diff --git a/unit/util/lower_byte_operators.cpp b/unit/util/lower_byte_operators.cpp index 155cb69213f..f8fa21b4adc 100644 --- a/unit/util/lower_byte_operators.cpp +++ b/unit/util/lower_byte_operators.cpp @@ -29,7 +29,7 @@ TEST_CASE("byte extract and bits", "[core][util][lowering][byte_extract]") cmdlinet cmdline; config.set(cmdline); - const auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; const unsignedbv_typet u16{16}; const exprt sixteen_bits = from_integer(0x1234, u16); @@ -98,7 +98,7 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]") cmdlinet cmdline; config.set(cmdline); - const auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("A byte_extract over a POD") { @@ -365,7 +365,7 @@ SCENARIO("byte_update_lowering", "[core][util][lowering][byte_update]") cmdlinet cmdline; config.set(cmdline); - const auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; GIVEN("A byte_update of a POD") { diff --git a/unit/util/pointer_offset_size.cpp b/unit/util/pointer_offset_size.cpp index 1da92d004e7..70ce2df0aee 100644 --- a/unit/util/pointer_offset_size.cpp +++ b/unit/util/pointer_offset_size.cpp @@ -25,7 +25,7 @@ TEST_CASE("Build subexpression to access element at offset into array") cmdlinet cmdline; config.set(cmdline); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; const signedbv_typet t(32); @@ -83,7 +83,7 @@ TEST_CASE("Build subexpression to access element at offset into struct") cmdlinet cmdline; config.set(cmdline); - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; const signedbv_typet t(32); diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index e041ca4e07e..41347348cc2 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -64,7 +64,7 @@ TEST_CASE("Simplify byte extract", "[core][util]") TEST_CASE("expr2bits and bits2expr respect bit order", "[core][util]") { - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); @@ -116,8 +116,6 @@ TEST_CASE("Simplify extractbit", "[core][util]") const cmdlinet cmdline; config.set(cmdline); - auto &ns = empty_namespace; - // binary: 1101 1110 1010 1101 1011 1110 1110 1111 // ^MSB LSB^ // bit23^ bit4^ @@ -126,13 +124,13 @@ TEST_CASE("Simplify extractbit", "[core][util]") const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); exprt eb1 = extractbit_exprt(deadbeef, 4); - bool unmodified = simplify(eb1, ns); + bool unmodified = simplify(eb1, empty_namespace); REQUIRE(!unmodified); REQUIRE(eb1 == false_exprt()); exprt eb2 = extractbit_exprt(deadbeef, 23); - unmodified = simplify(eb2, ns); + unmodified = simplify(eb2, empty_namespace); REQUIRE(!unmodified); REQUIRE(eb2 == true_exprt()); @@ -156,7 +154,7 @@ TEST_CASE("Simplify extractbits", "[core][util]") TEST_CASE("Simplify shift", "[core][util]") { - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; REQUIRE( simplify_expr(shl_exprt(from_integer(5, signedbv_typet(8)), 1), ns) == @@ -181,7 +179,7 @@ TEST_CASE("Simplify shift", "[core][util]") TEST_CASE("Simplify dynamic object comparison", "[core][util]") { - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; dynamic_object_exprt dynamic_object(signedbv_typet(8)); dynamic_object.set_instance(1); @@ -238,7 +236,7 @@ TEST_CASE("Simplify pointer_object equality", "[core][util]") TEST_CASE("Simplify cast from bool", "[core][util]") { - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; { // this checks that ((int)B)==1 turns into B @@ -291,7 +289,7 @@ TEST_CASE("Simplify cast from bool", "[core][util]") TEST_CASE("simplify_expr boolean expressions", "[core][util]") { - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; SECTION("Binary boolean operations") { @@ -515,8 +513,6 @@ TEST_CASE("Simplify bitor", "[core][util]") TEST_CASE("Simplify inequality", "[core][util]") { - auto &ns = empty_namespace; - { // This checks that 3 < (B ? 4 : 5) simplifies to true, just like (B ? 4 : // 5) > 3 simplifies to true. @@ -525,12 +521,12 @@ TEST_CASE("Simplify inequality", "[core][util]") if_exprt if_b{b, from_integer(4, sbv), from_integer(5, sbv)}; binary_relation_exprt comparison_gt{if_b, ID_gt, from_integer(3, sbv)}; - exprt simp = simplify_expr(comparison_gt, ns); + exprt simp = simplify_expr(comparison_gt, empty_namespace); REQUIRE(simp == true_exprt{}); binary_relation_exprt comparison_lt{from_integer(3, sbv), ID_lt, if_b}; - simp = simplify_expr(comparison_lt, ns); + simp = simplify_expr(comparison_lt, empty_namespace); REQUIRE(simp == true_exprt{}); } @@ -568,8 +564,6 @@ TEST_CASE("Simplify pointer cast of pointer arithmetic", "[core][util]") { config.set_arch("none"); - auto &ns = empty_namespace; - SECTION("Same element size: (char*)(unsigned_char_ptr + 1)") { // (char*)(ptr + 1) where ptr is unsigned char* should push the cast inside @@ -579,7 +573,7 @@ TEST_CASE("Simplify pointer cast of pointer arithmetic", "[core][util]") plus_exprt ptr_plus_1{ptr, from_integer(1, pointer_diff_type())}; typecast_exprt cast{ptr_plus_1, char_ptr_type}; - exprt result = simplify_expr(cast, ns); + exprt result = simplify_expr(cast, empty_namespace); // Expected: (char*)ptr + 1 plus_exprt expected{ @@ -596,7 +590,7 @@ TEST_CASE("Simplify pointer cast of pointer arithmetic", "[core][util]") plus_exprt ptr_plus_1{ptr, from_integer(1, pointer_diff_type())}; typecast_exprt cast{ptr_plus_1, char_ptr_type}; - exprt result = simplify_expr(cast, ns); + exprt result = simplify_expr(cast, empty_namespace); // Expected: (char*)ptr + 4 plus_exprt expected{ @@ -607,7 +601,7 @@ TEST_CASE("Simplify pointer cast of pointer arithmetic", "[core][util]") TEST_CASE("Simplify quantifier", "[core][util]") { - auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; SECTION("Simplification for exists") { diff --git a/unit/util/std_expr.cpp b/unit/util/std_expr.cpp index 1a5052e8c5e..91a1830af71 100644 --- a/unit/util/std_expr.cpp +++ b/unit/util/std_expr.cpp @@ -40,7 +40,7 @@ TEST_CASE("object descriptor expression", "[unit][util][std_expr]") { config.ansi_c.set_LP64(); - const auto &ns = empty_namespace; + const namespacet &ns = empty_namespace; array_typet array_type(signed_int_type(), from_integer(2, size_type())); struct_typet struct_type({{"foo", array_type}});