abstract_pointer_object.h

Go to the documentation of this file.

/*******************************************************************\
 
 Module: analyses variable-sensitivity
 
 Author: Thomas Kiley, thomas.kiley@diffblue.com
 
\*******************************************************************/
 
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
 
#include <analyses/variable-sensitivity/abstract_object.h>
 
class abstract_pointer_tag
{
};
 
class abstract_pointer_objectt : public abstract_objectt,
                                 public abstract_pointer_tag
{
public:
  explicit abstract_pointer_objectt(const typet &type);
 
  abstract_pointer_objectt(const typet &type, bool top, bool bottom);
 
  explicit abstract_pointer_objectt(
    const exprt &expr,
    const abstract_environmentt &environment,
    const namespacet &ns);
 
  abstract_object_pointert expression_transform(
    const exprt &expr,
    const std::vector<abstract_object_pointert> &operands,
    const abstract_environmentt &environment,
    const namespacet &ns) const override;
 
  abstract_object_pointert write(
    abstract_environmentt &environment,
    const namespacet &ns,
    const std::stack<exprt> &stack,
    const exprt &specifier,
    const abstract_object_pointert &value,
    bool merging_write) const override;
 
  void get_statistics(
    abstract_object_statisticst &statistics,
    abstract_object_visitedt &visited,
    const abstract_environmentt &env,
    const namespacet &ns) const override;
 
  virtual abstract_object_pointert read_dereference(
    const abstract_environmentt &env,
    const namespacet &ns) const = 0;
 
  virtual abstract_object_pointert write_dereference(
    abstract_environmentt &environment,
    const namespacet &ns,
    const std::stack<exprt> &stack,
    const abstract_object_pointert &value,
    bool merging_write) const = 0;
 
  virtual abstract_object_pointert typecast(
    const typet &new_type,
    const abstract_environmentt &environment,
    const namespacet &ns) const = 0;
 
  virtual abstract_object_pointert ptr_diff(
    const exprt &expr,
    const std::vector<abstract_object_pointert> &operands,
    const abstract_environmentt &environment,
    const namespacet &ns) const = 0;
 
  virtual exprt ptr_comparison_expr(
    const exprt &expr,
    const std::vector<abstract_object_pointert> &operands,
    const abstract_environmentt &environment,
    const namespacet &ns) const = 0;
 
private:
  abstract_object_pointert typecast_from_void_ptr(
    const exprt &expr,
    const std::vector<abstract_object_pointert> &operands,
    const abstract_environmentt &environment,
    const namespacet &ns) const;
  abstract_object_pointert eval_ptr_diff(
    const exprt &expr,
    const std::vector<abstract_object_pointert> &operands,
    const abstract_environmentt &environment,
    const namespacet &ns) const;
  abstract_object_pointert eval_ptr_comparison(
    const exprt &expr,
    const std::vector<abstract_object_pointert> &operands,
    const abstract_environmentt &environment,
    const namespacet &ns) const;
};
 
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H