replace_symbol.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_REPLACE_SYMBOL_H
#define CPROVER_UTIL_REPLACE_SYMBOL_H
 
//
// true: did nothing
// false: replaced something
//
 
#include "expr.h"
 
#include <set>
#include <unordered_map>
 
class replace_symbolt
{
public:
  typedef std::unordered_map<irep_idt, exprt> expr_mapt;
 
  void insert(const class symbol_exprt &old_expr,
              const exprt &new_expr);
 
  void set(const class symbol_exprt &old_expr, const exprt &new_expr);
 
  virtual bool replace(exprt &dest) const;
  virtual bool replace(typet &dest) const;
 
  void operator()(exprt &dest) const
  {
    replace(dest);
  }
  void operator()(exprt &dest) const {…}
 
  void operator()(typet &dest) const
  {
    replace(dest);
  }
  void operator()(typet &dest) const {…}
 
  void clear()
  {
    expr_map.clear();
  }
  void clear() {…}
 
  bool empty() const
  {
    return expr_map.empty();
  }
  bool empty() const {…}
 
  std::size_t erase(const irep_idt &id)
  {
    return expr_map.erase(id);
  }
  std::size_t erase(const irep_idt &id) {…}
 
  expr_mapt::iterator erase(expr_mapt::iterator it)
  {
    return expr_map.erase(it);
  }
  expr_mapt::iterator erase(expr_mapt::iterator it) {…}
 
  bool replaces_symbol(const irep_idt &id) const
  {
    return expr_map.find(id) != expr_map.end();
  }
  bool replaces_symbol(const irep_idt &id) const {…}
 
  replace_symbolt();
  virtual ~replace_symbolt();
 
  const expr_mapt &get_expr_map() const
  {
    return expr_map;
  }
  const expr_mapt &get_expr_map() const {…}
 
  expr_mapt &get_expr_map()
  {
    return expr_map;
  }
  expr_mapt &get_expr_map() {…}
 
protected:
  expr_mapt expr_map;
  mutable std::set<irep_idt> bindings;
 
  virtual bool replace_symbol_expr(symbol_exprt &dest) const;
 
  bool have_to_replace(const exprt &dest) const;
  bool have_to_replace(const typet &type) const;
};
class replace_symbolt {…};
 
class unchecked_replace_symbolt : public replace_symbolt
{
public:
  unchecked_replace_symbolt()
  {
  }
  unchecked_replace_symbolt() {…}
 
  void insert(const symbol_exprt &old_expr, const exprt &new_expr);
 
protected:
  bool replace_symbol_expr(symbol_exprt &dest) const override;
};
class unchecked_replace_symbolt : public replace_symbolt {…};
 
class address_of_aware_replace_symbolt : public unchecked_replace_symbolt
{
public:
  bool replace(exprt &dest) const override;
 
private:
  mutable bool require_lvalue = false;
 
  class set_require_lvalue_and_backupt
  {
  public:
    set_require_lvalue_and_backupt(bool &require_lvalue, const bool value)
      : require_lvalue(require_lvalue), prev_value(require_lvalue)
    {
      require_lvalue = value;
    }
    set_require_lvalue_and_backupt(bool &require_lvalue, const bool value) {…}
 
    ~set_require_lvalue_and_backupt()
    {
      require_lvalue = prev_value;
    }
    ~set_require_lvalue_and_backupt() {…}
 
  private:
    bool &require_lvalue;
    bool prev_value;
  };
  class set_require_lvalue_and_backupt {…};
 
  bool replace_symbol_expr(symbol_exprt &dest) const override;
};
class address_of_aware_replace_symbolt : public unchecked_replace_symbolt {…};
 
#endif // CPROVER_UTIL_REPLACE_SYMBOL_H