value_set_dereference.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Pointer Dereferencing
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
#define CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H
 
#include <util/std_expr.h>
 
class dereference_callbackt;
class messaget;
class symbol_tablet;
 
class value_set_dereferencet final
{
public:
  //    given dereference may follow a null pointer
  value_set_dereferencet(
    const namespacet &_ns,
    symbol_tablet &_new_symbol_table,
    dereference_callbackt &_dereference_callback,
    const irep_idt _language_mode,
    bool _exclude_null_derefs,
    const messaget &_log)
    : ns(_ns),
      new_symbol_table(_new_symbol_table),
      dereference_callback(_dereference_callback),
      language_mode(_language_mode),
      exclude_null_derefs(_exclude_null_derefs),
      log(_log)
  { }
 
  virtual ~value_set_dereferencet() { }
 
  exprt dereference(const exprt &pointer, bool display_points_to_sets = false);
 
  class valuet
  {
  public:
    exprt value;
    exprt pointer;
    exprt pointer_guard;
 
    valuet()
      : value{nil_exprt{}}, pointer{nil_exprt{}}, pointer_guard{false_exprt{}}
    {
    }
  };
 
  static bool should_ignore_value(
    const exprt &what,
    bool exclude_null_derefs,
    const irep_idt &language_mode);
 
  static valuet build_reference_to(
    const exprt &what,
    const exprt &pointer,
    const namespacet &ns);
 
  static bool dereference_type_compare(
    const typet &object_type,
    const typet &dereference_type,
    const namespacet &ns);
 
  static bool memory_model(
    exprt &value,
    const typet &type,
    const exprt &offset,
    const namespacet &ns);
 
  static bool memory_model_bytes(
    exprt &value,
    const typet &type,
    const exprt &offset,
    const namespacet &ns);
 
private:
  const namespacet &ns;
  symbol_tablet &new_symbol_table;
  dereference_callbackt &dereference_callback;
  const irep_idt language_mode;
  const bool exclude_null_derefs;
  const messaget &log;
  valuet get_failure_value(const exprt &pointer, const typet &type);
  exprt handle_dereference_base_case(
    const exprt &pointer,
    bool display_points_to_sets);
};
 
#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H