Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions unit/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
18 changes: 7 additions & 11 deletions unit/analyses/ai/ai_simplify_lhs.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,21 +9,18 @@ Author: Diffblue Ltd.
/// \file
/// Unit tests for ai_domain_baset::ai_simplify_lhs

#include <testing-utils/message.h>
#include <testing-utils/use_catch.h>

#include <analyses/ai_domain.h>

#include <ansi-c/ansi_c_language.h>

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/namespace.h>
#include <util/simplify_expr.h>
#include <util/symbol_table.h>
#include <util/ui_message.h>

#include <analyses/ai_domain.h>
#include <ansi-c/ansi_c_language.h>
#include <testing-utils/empty_namespace.h>
#include <testing-utils/message.h>
#include <testing-utils/use_catch.h>

class constant_simplification_mockt:public ai_domain_baset
{
public:
Expand Down Expand Up @@ -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;

Expand Down
4 changes: 0 additions & 4 deletions unit/analyses/does_remove_const/does_expr_lose_const.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,8 @@ Author: Diffblue Ltd.

#include <util/c_types.h>
#include <util/mathematical_types.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>

#include <goto-programs/goto_program.h>

Expand All @@ -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);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,25 +9,19 @@ Author: Diffblue Ltd.
/// \file
/// Does Remove Const Unit Tests

#include <testing-utils/use_catch.h>

#include <util/c_types.h>
#include <util/mathematical_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

#include <ansi-c/c_qualifiers.h>

#include <goto-programs/goto_program.h>

#include <analyses/does_remove_const/does_remove_const_util.h>
#include <analyses/does_remove_const.h>
#include <analyses/does_remove_const/does_remove_const_util.h>
#include <ansi-c/c_qualifiers.h>
#include <testing-utils/use_catch.h>

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);
Expand Down
12 changes: 3 additions & 9 deletions unit/analyses/does_remove_const/is_type_at_least_as_const_as.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,25 +9,19 @@ Author: Diffblue Ltd.
/// \file
/// Does Remove Const Unit Tests

#include <testing-utils/use_catch.h>

#include <util/c_types.h>
#include <util/mathematical_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

#include <ansi-c/c_qualifiers.h>

#include <goto-programs/goto_program.h>

#include <analyses/does_remove_const/does_remove_const_util.h>
#include <analyses/does_remove_const.h>
#include <analyses/does_remove_const/does_remove_const_util.h>
#include <ansi-c/c_qualifiers.h>
#include <testing-utils/use_catch.h>

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);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
#include <testing-utils/empty_namespace.h>

// NOLINTNEXTLINE(whitespace/line_length)
#include <analyses/variable-sensitivity/constant_abstract_value.h> // IWYU pragma: keep
Expand All @@ -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")
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,13 +9,13 @@
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/constant_abstract_value.h>
#include <analyses/variable-sensitivity/interval_abstract_value.h>
#include <analyses/variable-sensitivity/value_set_abstract_object.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <testing-utils/empty_namespace.h>
#include <testing-utils/use_catch.h>

#include "analyses/variable-sensitivity/variable_sensitivity_test_helpers.h"
Expand All @@ -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")
{
Expand Down Expand Up @@ -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")
Expand Down Expand Up @@ -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")
Expand Down
8 changes: 3 additions & 5 deletions unit/analyses/variable-sensitivity/abstract_object/merge.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,10 @@
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/abstract_object.h>
#include <testing-utils/empty_namespace.h>
#include <testing-utils/use_catch.h>

// NOLINTNEXTLINE(whitespace/line_length)
Expand Down Expand Up @@ -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);

Expand Down Expand Up @@ -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);

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,10 @@
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <testing-utils/empty_namespace.h>

// NOLINTNEXTLINE(whitespace/line_length)
#include <analyses/variable-sensitivity/constant_abstract_value.h> // IWYU pragma: keep
Expand Down Expand Up @@ -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")
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
#include <testing-utils/empty_namespace.h>

// NOLINTNEXTLINE(whitespace/line_length)
#include <analyses/variable-sensitivity/constant_abstract_value.h> // IWYU pragma: keep
Expand Down Expand Up @@ -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")
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,12 @@
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/constant_abstract_value.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
#include <testing-utils/empty_namespace.h>
#include <testing-utils/use_catch.h>

SCENARIO(
Expand All @@ -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")
{
Expand All @@ -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")
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,12 @@
#include <util/bitvector_types.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/symbol_table.h>

#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/constant_pointer_abstract_object.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
#include <testing-utils/empty_namespace.h>
#include <testing-utils/use_catch.h>

SCENARIO(
Expand All @@ -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")
{
Expand All @@ -56,7 +54,7 @@ SCENARIO(
{
const auto address_of = address_of_exprt(val2_symbol);
auto obj = std::make_shared<constant_pointer_abstract_objectt>(
address_of, environment, ns);
address_of, environment, empty_namespace);
THEN_PREDICATE(obj, "x == &val2");
}
}
Expand Down
5 changes: 2 additions & 3 deletions unit/analyses/variable-sensitivity/eval-member-access.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,13 @@

#include <util/arith_tools.h>
#include <util/mathematical_types.h>
#include <util/symbol_table.h>

#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/abstract_object.h>
#include <analyses/variable-sensitivity/context_abstract_object.h>
#include <analyses/variable-sensitivity/full_array_abstract_object.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <testing-utils/empty_namespace.h>
#include <testing-utils/use_catch.h>

void test_array(
Expand All @@ -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}")
{
Expand Down
Loading
Loading