type_size_mapping.h File Reference

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

#include <util/expr.h>
#include <solvers/smt2_incremental/ast/smt_terms.h>
#include <solvers/smt2_incremental/object_tracking.h>
#include <solvers/smt2_incremental/smt_is_dynamic_object.h>
#include <solvers/smt2_incremental/smt_object_size.h>
#include <unordered_map>

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

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.