validate_expressions.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Validate expressions
 
Author: Daniel Poetzl
 
\*******************************************************************/
 
#include "validate_expressions.h"
#include "validate_helpers.h"
 
#ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
#include <iostream>
#endif
 
#include "bitvector_expr.h" // IWYU pragma: keep
#include "pointer_expr.h"   // IWYU pragma: keep
#include "ssa_expr.h"
 
#define CALL_ON_EXPR(expr_type)                                                \
  C<exprt, expr_type>()(expr, std::forward<Args>(args)...)
 
template <template <typename, typename> class C, typename... Args>
void call_on_expr(const exprt &expr, Args &&... args)
{
  if(expr.id() == ID_equal)
  {
    CALL_ON_EXPR(equal_exprt);
  }
  else if(expr.id() == ID_plus)
  {
    CALL_ON_EXPR(plus_exprt);
  }
  else if(is_ssa_expr(expr))
  {
    CALL_ON_EXPR(ssa_exprt);
  }
  else if(expr.id() == ID_member)
  {
    CALL_ON_EXPR(member_exprt);
  }
  else if(expr.id() == ID_dereference)
  {
    CALL_ON_EXPR(dereference_exprt);
  }
  else if(expr.is_constant())
  {
    CALL_ON_EXPR(constant_exprt);
  }
  else if(expr.id() == ID_if)
  {
    CALL_ON_EXPR(if_exprt);
  }
  else if(expr.id() == ID_update)
  {
    CALL_ON_EXPR(update_exprt);
  }
  else if(expr.id() == ID_overflow_unary_minus)
  {
    CALL_ON_EXPR(unary_minus_overflow_exprt);
  }
  else if(expr.id() == ID_count_leading_zeros)
  {
    CALL_ON_EXPR(count_leading_zeros_exprt);
  }
  else
  {
#ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
    std::cerr << "Unimplemented well-formedness check for expression with id: "
              << expr.id_string() std::endl;
#endif
 
    CALL_ON_EXPR(exprt);
  }
}

void check_expr(const exprt &expr, const validation_modet vm)
{
  call_on_expr<call_checkt>(expr, vm);
}

void validate_expr(
  const exprt &expr,
  const namespacet &ns,
  const validation_modet vm)
{
  call_on_expr<call_validatet>(expr, ns, vm);
}

void validate_full_expr(
  const exprt &expr,
  const namespacet &ns,
  const validation_modet vm)
{
  call_on_expr<call_validate_fullt>(expr, ns, vm);
}