expr_util.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_EXPR_UTIL_H
#define CPROVER_UTIL_EXPR_UTIL_H
 
#include "irep.h"
 
#include <functional>
 
class constant_exprt;
class exprt;
class update_exprt;
class with_exprt;
class if_exprt;
class typet;
class namespacet;
 
bool is_assignable(const exprt &);
 
exprt make_binary(const exprt &);
 
with_exprt make_with_expr(const update_exprt &);
 
exprt is_not_zero(const exprt &, const namespacet &ns);
 
exprt boolean_negate(const exprt &);
 
bool has_subexpr(const exprt &, const std::function<bool(const exprt &)> &pred);
 
bool has_subexpr(const exprt &, const irep_idt &);
 
bool has_subtype(
  const typet &type,
  const std::function<bool(const typet &)> &pred,
  const namespacet &ns);
 
bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
 
if_exprt lift_if(const exprt &, std::size_t operand_number);
 
const exprt &skip_typecast(const exprt &expr);
 
class can_forward_propagatet
{
public:
  explicit can_forward_propagatet(const namespacet &ns) : ns(ns)
  {
  }
 
  bool operator()(const exprt &e) const
  {
    return is_constant(e);
  }
 
protected:
  const namespacet &ns;
 
  virtual bool is_constant(const exprt &) const;
  virtual bool is_constant_address_of(const exprt &) const;
};
 
constant_exprt make_boolean_expr(bool);
 
exprt make_and(exprt a, exprt b);
 
bool is_null_pointer(const constant_exprt &expr);
 
#endif // CPROVER_UTIL_EXPR_UTIL_H