value_set_abstract_object.h

Go to the documentation of this file.

/*******************************************************************\
 
 Module: analyses variable-sensitivity
 
 Author: diffblue
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
 
#include <analyses/variable-sensitivity/abstract_object_set.h>
#include <analyses/variable-sensitivity/abstract_value_object.h>
 
class value_set_abstract_objectt : public abstract_value_objectt,
                                   public value_set_tag
{
public:
  explicit value_set_abstract_objectt(const typet &type);
 
  value_set_abstract_objectt(const typet &type, bool top, bool bottom);
 
  value_set_abstract_objectt(
    const exprt &expr,
    const abstract_environmentt &environment,
    const namespacet &ns);
 
  static abstract_object_pointert
  make_value_set(const abstract_object_sett &initial_values);
 
  index_range_implementation_ptrt
  index_range_implementation(const namespacet &ns) const override;
 
  value_range_implementation_ptrt value_range_implementation() const override;
 
  exprt to_constant() const override;
  constant_interval_exprt to_interval() const override;
 
  abstract_value_pointert
  constrain(const exprt &lower, const exprt &upper) const override;
 
  const abstract_object_sett &get_values() const override
  {
    return values;
  }
 
  static const size_t max_value_set_size = 10;
 
  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
    const override;
 
protected:
  CLONE
 
  abstract_object_pointert merge_with_value(
    const abstract_value_pointert &other,
    const widen_modet &widen_mode) const override;
 
  abstract_object_pointert
  meet_with_value(const abstract_value_pointert &other) const override;
 
  exprt to_predicate_internal(const exprt &name) const override;
 
private:
  void set_values(const abstract_object_sett &other_values);
 
  abstract_object_pointert
  resolve_values(const abstract_object_sett &new_values) const;
 
  void set_top_internal() override;
 
  // data
  abstract_object_sett values;
};
 
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H