cbmc/type__size__mapping_8h_source.html

// 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

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

exprt
Base class for all expressions.
Definition expr.h:56

namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91

smt_function_application_termt::factoryt< smt_command_functiont >

expr.h

object_tracking.h
Data structures and algorithms used by smt2_incremental_decision_proceduret to track data about the o...

smt_object_mapt
std::unordered_map< exprt, decision_procedure_objectt, irep_hash > smt_object_mapt
Mapping from an object's base expression to the set of information about it which we track.
Definition object_tracking.h:91

object_size
exprt object_size(const exprt &pointer)
Definition pointer_predicates.cpp:33

smt_is_dynamic_object.h

smt_object_size.h

smt_terms.h

associate_pointer_sizes
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)
This function populates the (pointer) type -> size map.
Definition type_size_mapping.cpp:13

type_size_mapt
std::unordered_map< typet, smt_termt, irep_hash > type_size_mapt
Definition type_size_mapping.h:18