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>
 
#include <solvers/smt2_incremental/object_tracking.h>
#include <solvers/smt2_incremental/smt_object_size.h>
#include <solvers/smt2_incremental/smt_terms.h>
 
#include <unordered_map>
 
using type_size_mapt = std::unordered_map<typet, smt_termt, irep_full_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);
 
#endif