Skip to content

Commit b5c55b3

Browse files
author
thk123
committed
Added utility functions for checking expressions
Use namespace rather than class with static functions as more semantically correct.
1 parent 2779399 commit b5c55b3

File tree

3 files changed

+119
-5
lines changed

3 files changed

+119
-5
lines changed

unit/Makefile

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,17 @@
11
.PHONY: all cprover.dir test
22

3-
SRC = unit_tests.cpp \
4-
analyses/does_remove_const/does_expr_lose_const.cpp \
5-
analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
6-
analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
7-
catch_example.cpp \
3+
# Source files for test utilities
4+
SRC = src/expr/require_expr.cpp \
85
# Empty last line
96

7+
# Test source files
8+
SRC += unit_tests.cpp \
9+
analyses/does_remove_const/does_expr_lose_const.cpp \
10+
analyses/does_remove_const/does_type_preserve_const_correctness.cpp \
11+
analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
12+
catch_example.cpp \
13+
# Empty last line
14+
1015
INCLUDES= -I ../src/ -I.
1116

1217
include ../src/config.inc

unit/src/expr/require_expr.cpp

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test utilities
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Helper functions for requiring specific expressions
11+
/// If the expression is of the wrong type, throw a CATCH exception
12+
/// Also checks associated properties and returns a casted version of the
13+
/// expression.
14+
15+
#include "require_expr.h"
16+
17+
#include <catch.hpp>
18+
#include <util/arith_tools.h>
19+
20+
/// Verify a given exprt is an index_exprt with a a constant value equal to the
21+
/// expected value
22+
/// \param expr: The expression.
23+
/// \param expected_index: The constant value that should be the index.
24+
/// \return The expr cast to an index_exprt
25+
index_exprt require_expr::require_index(const exprt &expr, int expected_index)
26+
{
27+
REQUIRE(expr.id()==ID_index);
28+
const index_exprt &index_expr=to_index_expr(expr);
29+
REQUIRE(index_expr.index().id()==ID_constant);
30+
const constant_exprt &index_value=to_constant_expr(index_expr.index());
31+
mp_integer index_integer_value;
32+
to_integer(index_value, index_integer_value);
33+
REQUIRE(index_integer_value==expected_index);
34+
35+
return index_expr;
36+
}
37+
38+
/// Verify a given exprt is an index_exprt with a nil value as its index
39+
/// \param expr: The expression.
40+
/// \return The expr cast to an index_exprt
41+
index_exprt require_expr::require_top_index(const exprt &expr)
42+
{
43+
REQUIRE(expr.id()==ID_index);
44+
const index_exprt &index_expr=to_index_expr(expr);
45+
REQUIRE(index_expr.index().id()==ID_nil);
46+
return index_expr;
47+
}
48+
49+
/// Verify a given exprt is an member_exprt with a component name equal to the
50+
/// component_identifier
51+
/// \param expr: The expression.
52+
/// \param component_identifier: The name of the component that should be being
53+
/// accessed.
54+
/// \return The expr cast to a member_exprt.
55+
member_exprt require_expr::require_member(
56+
const exprt &expr, const irep_idt &component_identifier)
57+
{
58+
REQUIRE(expr.id()==ID_member);
59+
const member_exprt &member_expr=to_member_expr(expr);
60+
REQUIRE(member_expr.get_component_name()==component_identifier);
61+
return member_expr;
62+
}
63+
64+
/// Verify a given exprt is an symbol_exprt with a identifier name equal to the
65+
/// symbol_name.
66+
/// \param expr: The expression.
67+
/// \param symbol_name: The intended identifier of the symbol
68+
/// \return The expr cast to a symbol_exprt
69+
symbol_exprt require_expr::require_symbol(
70+
const exprt &expr, const irep_idt &symbol_name)
71+
{
72+
REQUIRE(expr.id()==ID_symbol);
73+
const symbol_exprt &symbol_expr=to_symbol_expr(expr);
74+
REQUIRE(symbol_expr.get_identifier()==symbol_name);
75+
return symbol_expr;
76+
}

unit/src/expr/require_expr.h

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
/*******************************************************************\
2+
3+
Module: Unit test utilities
4+
5+
Author: DiffBlue Limited. All rights reserved.
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Helper functions for requiring specific expressions
11+
/// If the expression is of the wrong type, throw a CATCH exception
12+
/// Also checks associated properties and returns a casted version of the
13+
/// expression.
14+
15+
#ifndef CPROVER_SRC_EXPR_REQUIRE_EXPR_H
16+
#define CPROVER_SRC_EXPR_REQUIRE_EXPR_H
17+
18+
#include <util/std_expr.h>
19+
20+
// NOLINTNEXTLINE(readability/namespace)
21+
namespace require_expr
22+
{
23+
index_exprt require_index(const exprt &expr, int expected_index);
24+
index_exprt require_top_index(const exprt &expr);
25+
26+
member_exprt require_member(
27+
const exprt &expr, const irep_idt &component_identifier);
28+
29+
symbol_exprt require_symbol(
30+
const exprt &expr, const irep_idt &symbol_name);
31+
}
32+
33+
#endif // CPROVER_SRC_EXPR_REQUIRE_EXPR_H

0 commit comments

Comments
 (0)