File: require_expr.cpp

package info (click to toggle)
cbmc 6.6.0-4
  • links: PTS
  • area: main
  • in suites: forky, sid, trixie
  • size: 153,852 kB
  • sloc: cpp: 386,459; ansic: 114,466; java: 28,405; python: 6,003; yacc: 4,552; makefile: 4,041; lex: 2,487; xml: 2,388; sh: 2,050; perl: 557; pascal: 184; javascript: 163; ada: 36
file content (107 lines) | stat: -rw-r--r-- 3,667 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
/*******************************************************************\

Module: Unit test utilities

Author: Diffblue Ltd.

\*******************************************************************/

/// \file
/// Helper functions for requiring specific expressions
/// If the expression is of the wrong type, throw a CATCH exception
/// Also checks associated properties and returns a casted version of the
/// expression.

#include "require_expr.h"

#include <testing-utils/use_catch.h>
#include <util/arith_tools.h>
#include <util/std_code.h>

/// Verify a given exprt is an index_exprt with a a constant value equal to the
/// expected value
/// \param expr: The expression.
/// \param expected_index: The constant value that should be the index.
/// \return The expr cast to an index_exprt
index_exprt require_expr::require_index(const exprt &expr, int expected_index)
{
  REQUIRE(expr.id()==ID_index);
  const index_exprt &index_expr=to_index_expr(expr);
  REQUIRE(index_expr.index().is_constant());
  const mp_integer index_integer_value =
    numeric_cast_v<mp_integer>(to_constant_expr(index_expr.index()));
  REQUIRE(index_integer_value==expected_index);

  return index_expr;
}

/// Verify a given exprt is an index_exprt with a nil value as its index
/// \param expr: The expression.
/// \return The expr cast to an index_exprt
index_exprt require_expr::require_top_index(const exprt &expr)
{
  REQUIRE(expr.id()==ID_index);
  const index_exprt &index_expr=to_index_expr(expr);
  REQUIRE(index_expr.index().id()==ID_nil);
  return index_expr;
}

/// Verify a given exprt is an member_exprt with a component name equal to the
/// component_identifier
/// \param expr: The expression.
/// \param component_identifier: The name of the component that should be being
///   accessed.
/// \return The expr cast to a member_exprt.
member_exprt require_expr::require_member(
  const exprt &expr, const irep_idt &component_identifier)
{
  REQUIRE(expr.id()==ID_member);
  const member_exprt &member_expr=to_member_expr(expr);
  REQUIRE(member_expr.get_component_name()==component_identifier);
  return member_expr;
}

/// Verify a given exprt is an symbol_exprt with a identifier name equal to the
/// symbol_name.
/// \param expr: The expression.
/// \param symbol_name: The intended identifier of the symbol
/// \return The expr cast to a symbol_exprt
symbol_exprt require_expr::require_symbol(
  const exprt &expr, const irep_idt &symbol_name)
{
  const symbol_exprt &symbol_expr = require_symbol(expr);
  REQUIRE(symbol_expr.get_identifier()==symbol_name);
  return symbol_expr;
}

/// Verify a given exprt is a symbol_exprt.
/// \param expr: The expression.
/// \return The expr cast to a symbol_exprt
symbol_exprt require_expr::require_symbol(const exprt &expr)
{
  REQUIRE(expr.id() == ID_symbol);
  return to_symbol_expr(expr);
}

/// Verify a given exprt is a typecast_expr.
/// \param expr: The expression.
/// \return The expr cast to a typecast_exprt
typecast_exprt require_expr::require_typecast(const exprt &expr)
{
  REQUIRE(expr.id() == ID_typecast);
  return to_typecast_expr(expr);
}

/// Verify a given exprt is a side_effect_exprt with appropriate statement.
/// \param expr: The expression.
/// \param side_effect_statement: The kind of side effect that is required
/// \return The expr cast to a side_effect_exprt
side_effect_exprt require_expr::require_side_effect_expr(
  const exprt &expr,
  const irep_idt &side_effect_statement)
{
  REQUIRE(expr.id() == ID_side_effect);
  const side_effect_exprt &side_effect_expr = to_side_effect_expr(expr);
  REQUIRE(side_effect_expr.get_statement() == side_effect_statement);
  return side_effect_expr;
}