type_size_mapping.cpp File Reference

#include "type_size_mapping.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/invariant.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <solvers/smt2_incremental/convert_expr_to_smt.h>

Include dependency graph for type_size_mapping.cpp:

Go to the source code of this file.

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

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

expression	the expression we're building the map for.
ns	A 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_map	A 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_map	passed through to convert_expr_to_smt
object_size	passed through to convert_expr_to_smt
is_dynamic_object	passed through to convert_expr_to_smt

Definition at line 13 of file type_size_mapping.cpp.