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

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:94

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