object_tracking.h

Go to the documentation of this file.

// Author: Diffblue Ltd.

 
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H
 
#include <util/expr.h>
#include <util/pointer_expr.h>
 
#include <unordered_map>

struct decision_procedure_objectt
{
  exprt base_expression;
  std::size_t unique_id = 0;
  exprt size;
  bool is_dynamic = false;
};

exprt find_object_base_expression(const address_of_exprt &address_of);

template <typename output_object_functiont>
void find_object_base_expressions(
  const exprt &expression,
  const output_object_functiont &output_object)
{
  expression.visit_pre([&](const exprt &node) {
    if(const auto address_of = expr_try_dynamic_cast<address_of_exprt>(node))
    {
      output_object(find_object_base_expression(*address_of));
    }
  });
}

using smt_object_mapt =
  std::unordered_map<exprt, decision_procedure_objectt, irep_hash>;

smt_object_mapt initial_smt_object_map();

void track_expression_objects(
  const exprt &expression,
  const namespacet &ns,
  smt_object_mapt &object_map);

bool objects_are_already_tracked(
  const exprt &expression,
  const smt_object_mapt &object_map);

exprt make_invalid_pointer_expr();
 
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_OBJECT_TRACKING_H