type_size_mapping.h

Go to the documentation of this file.

// Author: Diffblue Ltd.

 
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_SIZE_MAPPING_H
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_SIZE_MAPPING_H
 
#include <util/expr.h> // IWYU pragma: keep
 
#include <solvers/smt2_incremental/ast/smt_terms.h>   // IWYU pragma: keep
#include <solvers/smt2_incremental/object_tracking.h> // IWYU pragma: keep
#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
#include <solvers/smt2_incremental/smt_object_size.h> // IWYU pragma: keep
 
#include <unordered_map> // IWYU pragma: keep
 
using type_size_mapt = std::unordered_map<typet, smt_termt, irep_hash>;

void associate_pointer_sizes(
  const exprt &expression,
  const namespacet &ns,
  type_size_mapt &type_size_map,
  const smt_object_mapt &object_map,
  const smt_object_sizet::make_applicationt &object_size,
  const smt_is_dynamic_objectt::make_applicationt &is_dynamic_object);
 
#endif