std_code_base.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Data structures representing statements in a program
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_STD_CODE_BASE_H
#define CPROVER_UTIL_STD_CODE_BASE_H
 
#include "expr_cast.h"
#include "invariant.h"
#include "std_types.h"
#include "validate.h"

class codet : public exprt
{
public:
  explicit codet(const irep_idt &statement) : exprt(ID_code, empty_typet())
  {
    set_statement(statement);
  }
 
  codet(const irep_idt &statement, source_locationt loc)
    : exprt(ID_code, empty_typet(), std::move(loc))
  {
    set_statement(statement);
  }

  explicit codet(const irep_idt &statement, operandst _op) : codet(statement)
  {
    operands() = std::move(_op);
  }
 
  codet(const irep_idt &statement, operandst op, source_locationt loc)
    : codet(statement, std::move(loc))
  {
    operands() = std::move(op);
  }
 
  void set_statement(const irep_idt &statement)
  {
    set(ID_statement, statement);
  }
 
  const irep_idt &get_statement() const
  {
    return get(ID_statement);
  }
 
  codet &first_statement();
  const codet &first_statement() const;
  codet &last_statement();
  const codet &last_statement() const;
 
  using exprt::op0;
  using exprt::op1;
  using exprt::op2;
  using exprt::op3;
};
 
namespace detail // NOLINT
{
template <typename Tag>
inline bool can_cast_code_impl(const exprt &expr, const Tag &tag)
{
  if(const auto ptr = expr_try_dynamic_cast<codet>(expr))
  {
    return ptr->get_statement() == tag;
  }
  return false;
}
 
} // namespace detail
 
template <>
inline bool can_cast_expr<codet>(const exprt &base)
{
  return base.id() == ID_code;
}
 
// to_code has no validation other than checking the id(), so no validate_expr
// is provided for codet
 
inline const codet &to_code(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_code);
  return static_cast<const codet &>(expr);
}
 
inline codet &to_code(exprt &expr)
{
  PRECONDITION(expr.id() == ID_code);
  return static_cast<codet &>(expr);
}
 
#endif // CPROVER_UTIL_STD_CODE_BASE_H