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/analyses/ai/ai_simplify_lhs.cpp b/unit/analyses/ai/ai_simplify_lhs.cpp index 7e38f26f392..96e6b0cd735 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); + const namespacet &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..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,10 +11,8 @@ Author: Diffblue Ltd. #include #include -#include #include #include -#include #include @@ -26,8 +24,6 @@ Author: Diffblue Ltd. 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..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 @@ -9,25 +9,19 @@ Author: Diffblue Ltd. /// \file /// Does Remove Const Unit Tests -#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..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 @@ -9,25 +9,19 @@ Author: Diffblue Ltd. /// \file /// Does Remove Const Unit Tests -#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..c5b3f7a4ef6 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); + 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 31a30119f05..424da3c94b9 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); + const namespacet &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); + const namespacet &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); + 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 fb5b00fd275..88f57b3482a 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,13 +93,11 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); 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); @@ -138,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 26b500e73cd..eed4e4ef71e 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); + 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 10fffe551e5..17099429e22 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); + 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 a5358355321..d82c5fbaa67 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,6 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); GIVEN("constant_abstract_value") { @@ -51,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 ce37c9ca7cc..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 @@ -9,12 +9,12 @@ #include #include #include -#include #include #include #include #include +#include #include SCENARIO( @@ -35,8 +35,6 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); GIVEN("constant_pointer_abstract_object") { @@ -56,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 3fd4c3537ad..dceb954181b 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}; + 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 8ec9733cf23..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 @@ -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); + 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 140279e4855..420cc7b1634 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); + 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 263244fcbc1..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 @@ -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); + 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 4efe8b4f6ba..88f27cbbe14 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); + 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 2ad91a4e383..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 @@ -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); + 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 be191ecfc9f..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 @@ -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}; + 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 8d2d97029d4..c00b94ff09c 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); + 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 8951fd2c0d8..42802d98f10 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); + 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 91941c97dd7..cdce7f95f6c 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,6 @@ SCENARIO( variable_sensitivity_object_factoryt::configured_with(config); abstract_environmentt environment{object_factory}; environment.make_top(); - symbol_tablet symbol_table; - namespacet ns(symbol_table); GIVEN("interval_abstract_value") { @@ -61,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 4f0a7bdfd73..438b18fbbb6 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); + 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 f26e0da09b5..bf0786ee569 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); + 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 18c7e0b86ca..0600cfd31ba 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); + 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 a33d432cb3f..75b5f081630 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); + 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 1baefda7468..2af278484e9 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}; + 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 32d87327c6d..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 @@ -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}; + 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 e354520d407..58730924665 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); + 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 31eb26d9148..c2513b7452a 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}; + 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 e37287e2b30..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 @@ -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); + 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 8f85268795d..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 @@ -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); + 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 ed8cf002a4d..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 @@ -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); + 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 aa149ae0383..b5dec0c7563 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); + const namespacet &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/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/goto-programs/goto_trace_output.cpp b/unit/goto-programs/goto_trace_output.cpp index 729d5ca2b50..28b7d6f1c16 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,6 @@ SCENARIO( "Output trace with nil lhs object", "[core][goto-programs][goto_trace]") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); goto_programt::instructionst instructions; instructions.emplace_back(goto_program_instruction_typet::OTHER); goto_trace_stept step; @@ -29,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 dac9d344111..0bd4a1af12e 100644 --- a/unit/goto-programs/xml_expr.cpp +++ b/unit/goto-programs/xml_expr.cpp @@ -6,25 +6,22 @@ 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 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"); @@ -33,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 29bb54a7d6f..27c441b9b43 100644 --- a/unit/goto-symex/is_constant.cpp +++ b/unit/goto-symex/is_constant.cpp @@ -9,22 +9,19 @@ 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}; - 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/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..ee40fff6a6e 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,11 +201,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x&!x==0") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); 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); @@ -220,11 +217,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x+x==1") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); 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); @@ -237,11 +232,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*y==y*x") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); 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); @@ -255,11 +248,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*x==2") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); 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); @@ -272,11 +263,9 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") GIVEN("A bdd for x*x==4") { - symbol_tablet symbol_table; - namespacet ns(symbol_table); 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); @@ -334,9 +323,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/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 diff --git a/unit/solvers/flattening/boolbv.cpp b/unit/solvers/flattening/boolbv.cpp index a3ca65f32f5..9f0bde9234a 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,9 +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); - 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 521d99e8108..484db42896c 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,9 +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}; - 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 c2ee0d45fcb..509652dfe39 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,9 +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}; - 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 b8b13336798..3fbc8bca877 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,9 +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}; - 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/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..aea2daf2762 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,12 +469,11 @@ 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}; - 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, @@ -545,12 +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 symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - 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, @@ -577,12 +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 symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - 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, @@ -615,12 +612,11 @@ 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}; - 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, @@ -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 namespacet &ns = empty_namespace; const symbol_exprt foo{"foo", unsignedbv_typet{32}}; const symbol_exprt bar{"bar", unsignedbv_typet{32}}; SECTION("Address of symbol") @@ -1674,12 +1669,10 @@ 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 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; @@ -1699,11 +1692,9 @@ 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 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; @@ -1723,8 +1714,6 @@ 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 typet value_type = signedbv_typet{8}; const exprt array = symbol_exprt{ "my_array", array_typet{value_type, from_integer(10, signed_size_type())}}; @@ -1756,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/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..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 @@ -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,12 +24,10 @@ static exprt actual( const unsigned long radix_ul) { const constant_exprt chr = from_integer(character, char_type); - symbol_tablet symtab; - const namespacet ns(symtab); 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 f4833a812ab..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 @@ -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,13 +23,11 @@ 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); 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 8148114e727..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 @@ -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 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 d2afe05f39b..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 @@ -7,11 +7,11 @@ Author: Diffblue Ltd. \*******************************************************************/ -#include +#include #include -#include -#include +#include +#include SCENARIO( "length_of_decimal_int", @@ -19,9 +19,6 @@ SCENARIO( { const typet type = signedbv_typet(32); - const symbol_tablet symbol_table; - const namespacet ns{symbol_table}; - 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}; @@ -39,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); } @@ -58,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 d86abcec0e5..468914e852c 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,9 +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}; - info.ns = &ns; + info.ns = &empty_namespace; satcheckt sat_solver{log}; info.prop = &sat_solver; 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..ac9ab758521 --- /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_namespace.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..b5d156ccda1 --- /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 diff --git a/unit/util/bitvector_expr.cpp b/unit/util/bitvector_expr.cpp index bf4207fa11f..faac4794a7d 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,9 +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}; - 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/add.cpp b/unit/util/interval/add.cpp index 45699877759..5119fea0fb3 100644 --- a/unit/util/interval/add.cpp +++ b/unit/util/interval/add.cpp @@ -3,13 +3,11 @@ Author: DiffBlue Limited \*******************************************************************/ -#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 +17,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..d37a24c3d07 100644 --- a/unit/util/interval/comparisons.cpp +++ b/unit/util/interval/comparisons.cpp @@ -3,13 +3,11 @@ Author: DiffBlue Limited \*******************************************************************/ -#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 +17,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..5d5a3609ed9 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); + const namespacet &ns = empty_namespace; std::vector ve; diff --git a/unit/util/interval/modulo.cpp b/unit/util/interval/modulo.cpp index 895a995c4c1..972d4fdb55f 100644 --- a/unit/util/interval/modulo.cpp +++ b/unit/util/interval/modulo.cpp @@ -3,13 +3,11 @@ Author: DiffBlue Limited \*******************************************************************/ -#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 +36,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..92272aeeeaf 100644 --- a/unit/util/interval/multiply.cpp +++ b/unit/util/interval/multiply.cpp @@ -3,13 +3,11 @@ Author: DiffBlue Limited \*******************************************************************/ -#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 +17,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..7240abe6e66 100644 --- a/unit/util/interval/subtract.cpp +++ b/unit/util/interval/subtract.cpp @@ -3,13 +3,11 @@ Author: DiffBlue Limited \*******************************************************************/ -#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 +17,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..f8fa21b4adc 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 namespacet &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 namespacet &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 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 a091f1c7f42..70ce2df0aee 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); + const namespacet &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); + 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 663b5b19325..41347348cc2 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); + const namespacet &ns = empty_namespace; exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); @@ -122,9 +116,6 @@ TEST_CASE("Simplify extractbit", "[core][util]") const cmdlinet cmdline; config.set(cmdline); - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); - // binary: 1101 1110 1010 1101 1011 1110 1110 1111 // ^MSB LSB^ // bit23^ bit4^ @@ -133,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()); @@ -152,13 +143,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 +154,7 @@ TEST_CASE("Simplify extractbits", "[core][util]") TEST_CASE("Simplify shift", "[core][util]") { - const symbol_tablet symbol_table; - const namespacet ns(symbol_table); + const namespacet &ns = empty_namespace; REQUIRE( simplify_expr(shl_exprt(from_integer(5, signedbv_typet(8)), 1), ns) == @@ -192,8 +179,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); + const namespacet &ns = empty_namespace; dynamic_object_exprt dynamic_object(signedbv_typet(8)); dynamic_object.set_instance(1); @@ -238,23 +224,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); + const namespacet &ns = empty_namespace; { // this checks that ((int)B)==1 turns into B @@ -307,8 +289,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}; + const namespacet &ns = empty_namespace; SECTION("Binary boolean operations") { @@ -520,24 +501,18 @@ 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); - { // This checks that 3 < (B ? 4 : 5) simplifies to true, just like (B ? 4 : // 5) > 3 simplifies to true. @@ -546,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{}); } @@ -561,30 +536,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,9 +564,6 @@ TEST_CASE("Simplify pointer cast of pointer arithmetic", "[core][util]") { config.set_arch("none"); - symbol_tablet symbol_table; - namespacet ns(symbol_table); - SECTION("Same element size: (char*)(unsigned_char_ptr + 1)") { // (char*)(ptr + 1) where ptr is unsigned char* should push the cast inside @@ -604,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{ @@ -621,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{ @@ -632,8 +601,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}; + const namespacet &ns = empty_namespace; SECTION("Simplification for exists") { @@ -656,57 +624,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 +667,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 +679,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..91a1830af71 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 namespacet &ns = empty_namespace; array_typet array_type(signed_int_type(), from_integer(2, size_type())); struct_typet struct_type({{"foo", array_type}});