Skip to content

Commit 46fa176

Browse files
author
thk123
committed
Extending require utilities to be used in test
1 parent 6df8d6b commit 46fa176

File tree

2 files changed

+43
-2
lines changed

2 files changed

+43
-2
lines changed

unit/testing-utils/require_expr.cpp

+34-2
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616

1717
#include <testing-utils/catch.hpp>
1818
#include <util/arith_tools.h>
19+
#include <util/std_code.h>
1920

2021
/// Verify a given exprt is an index_exprt with a a constant value equal to the
2122
/// expected value
@@ -69,8 +70,39 @@ member_exprt require_expr::require_member(
6970
symbol_exprt require_expr::require_symbol(
7071
const exprt &expr, const irep_idt &symbol_name)
7172
{
72-
REQUIRE(expr.id()==ID_symbol);
73-
const symbol_exprt &symbol_expr=to_symbol_expr(expr);
73+
const symbol_exprt &symbol_expr = require_symbol(expr);
7474
REQUIRE(symbol_expr.get_identifier()==symbol_name);
7575
return symbol_expr;
7676
}
77+
78+
/// Verify a given exprt is a symbol_exprt.
79+
/// \param expr: The expression.
80+
/// \return The expr cast to a symbol_exprt
81+
symbol_exprt require_expr::require_symbol(const exprt &expr)
82+
{
83+
REQUIRE(expr.id() == ID_symbol);
84+
return to_symbol_expr(expr);
85+
}
86+
87+
/// Verify a given exprt is a typecast_expr.
88+
/// \param expr: The expression.
89+
/// \return The expr cast to a typecast_exprt
90+
typecast_exprt require_expr::require_typecast(const exprt &expr)
91+
{
92+
REQUIRE(expr.id() == ID_typecast);
93+
return to_typecast_expr(expr);
94+
}
95+
96+
/// Verify a given exprt is a side_effect_exprt with appropriate statement.
97+
/// \param expr: The expression.
98+
/// \param symbol_name: The intended identifier of statement
99+
/// \return The expr cast to a side_effect_exprt
100+
side_effect_exprt require_expr::require_side_effect_expr(
101+
const exprt &expr,
102+
const irep_idt &side_effect_statement)
103+
{
104+
REQUIRE(expr.id() == ID_side_effect);
105+
const side_effect_exprt &side_effect_expr = to_side_effect_expr(expr);
106+
REQUIRE(side_effect_expr.get_statement() == side_effect_statement);
107+
return side_effect_expr;
108+
}

unit/testing-utils/require_expr.h

+9
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616
#define CPROVER_TESTING_UTILS_REQUIRE_EXPR_H
1717

1818
#include <util/std_expr.h>
19+
#include <util/std_code.h>
1920

2021
// NOLINTNEXTLINE(readability/namespace)
2122
namespace require_expr
@@ -28,6 +29,14 @@ namespace require_expr
2829

2930
symbol_exprt require_symbol(
3031
const exprt &expr, const irep_idt &symbol_name);
32+
33+
symbol_exprt require_symbol(const exprt &expr);
34+
35+
typecast_exprt require_typecast(const exprt &expr);
36+
37+
side_effect_exprt require_side_effect_expr(
38+
const exprt &expr,
39+
const irep_idt &side_effect_statement);
3140
}
3241

3342
#endif // CPROVER_TESTING_UTILS_REQUIRE_EXPR_H

0 commit comments

Comments
 (0)