require_expr.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Unit test utilities
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
 
#include "require_expr.h"
 
#include <testing-utils/use_catch.h>
#include <util/arith_tools.h>
#include <util/std_code.h>
 
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().id()==ID_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;
}
 
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;
}
 
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;
}
 
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;
}
 
symbol_exprt require_expr::require_symbol(const exprt &expr)
{
  REQUIRE(expr.id() == ID_symbol);
  return to_symbol_expr(expr);
}
 
typecast_exprt require_expr::require_typecast(const exprt &expr)
{
  REQUIRE(expr.id() == ID_typecast);
  return to_typecast_expr(expr);
}
 
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;
}