CBMC
type_size_mapping.h File Reference

Utilities for making a map of types to associated sizes. More...

+ Include dependency graph for type_size_mapping.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Typedefs

using type_size_mapt = std::unordered_map< typet, smt_termt, irep_hash >
 

Functions

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. More...
 

Detailed Description

Utilities for making a map of types to associated sizes.

Definition in file type_size_mapping.h.

Typedef Documentation

◆ type_size_mapt

using type_size_mapt = std::unordered_map<typet, smt_termt, irep_hash>

Definition at line 18 of file type_size_mapping.h.

Function Documentation

◆ 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.

Parameters
expressionthe expression we're building the map for.
nsA namespace - passed to size_of_expr to lookup type symbols in case the pointers have type tag_typet, rather than a more completely defined type.
type_size_mapA map of types to terms expressing the size of the type (in bytes). This function adds new entries to the map for instances of pointer.base_type() from expression which are not already keys in the map.
object_mappassed through to convert_expr_to_smt
object_sizepassed through to convert_expr_to_smt
is_dynamic_objectpassed through to convert_expr_to_smt

Definition at line 13 of file type_size_mapping.cpp.