write_stack_entry.cpp

Go to the documentation of this file.

/*******************************************************************\
 
 Module: Analyses Variable Sensitivity
 
 Author: DiffBlue Limited.
 
\*******************************************************************/
 
 
#include <unordered_set>
 
#include "abstract_environment.h"
#include "write_stack_entry.h"
 
bool write_stack_entryt::try_squash_in(
  std::shared_ptr<const write_stack_entryt> new_entry,
  const abstract_environmentt &enviroment,
  const namespacet &ns)
{
  return false;
}
bool write_stack_entryt::try_squash_in( {…}
 
simple_entryt::simple_entryt(exprt expr) : simple_entry(expr)
{
  // Invalid simple expression added to the stack
  PRECONDITION(
    expr.id() == ID_member || expr.id() == ID_symbol ||
    expr.id() == ID_dynamic_object);
}
simple_entryt::simple_entryt(exprt expr) : simple_entry(expr) {…}
 
std::pair<exprt, bool> simple_entryt::get_access_expr() const
{
  return {simple_entry, false};
}
std::pair<exprt, bool> simple_entryt::get_access_expr() const {…}
 
offset_entryt::offset_entryt(abstract_object_pointert offset_value)
  : offset(offset_value)
{
  // The type of the abstract object should be an integral number
  static const std::unordered_set<irep_idt, irep_id_hash> integral_types = {
    ID_signedbv, ID_unsignedbv, ID_integer};
  PRECONDITION(
    integral_types.find(offset_value->type().id()) != integral_types.cend());
}
offset_entryt::offset_entryt(abstract_object_pointert offset_value) {…}
 
std::pair<exprt, bool> offset_entryt::get_access_expr() const
{
  return {offset->to_constant(), true};
}
std::pair<exprt, bool> offset_entryt::get_access_expr() const {…}
 
bool offset_entryt::try_squash_in(
  std::shared_ptr<const write_stack_entryt> new_entry,
  const abstract_environmentt &enviroment,
  const namespacet &ns)
{
  std::shared_ptr<const offset_entryt> cast_entry =
    std::dynamic_pointer_cast<const offset_entryt>(new_entry);
  if(cast_entry)
  {
    plus_exprt result_offset(
      cast_entry->offset->to_constant(), offset->to_constant());
    offset = enviroment.eval(result_offset, ns);
    return true;
  }
  return false;
}
bool offset_entryt::try_squash_in( {…}