construct_value_expr_from_smt.cpp File Reference

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/type.h>
#include <solvers/smt2_incremental/ast/smt_terms.h>
#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>

Include dependency graph for construct_value_expr_from_smt.cpp:

Go to the source code of this file.

Classes
class	value_expr_from_smt_factoryt

Functions
exprt	construct_value_expr_from_smt (const smt_termt &value_term, const typet &type_to_construct, const namespacet &ns)
	Given a value_term and a type_to_construct, this function constructs a value exprt with a value based on value_term and a type of type_to_construct.

Function Documentation

construct_value_expr_from_smt()

exprt construct_value_expr_from_smt	(	const smt_termt &	value_term,
		const typet &	type_to_construct,
		const namespacet &	ns )

Given a value_term and a type_to_construct, this function constructs a value exprt with a value based on value_term and a type of type_to_construct.

Parameters

value_term	This must be a "simple" term encoding a value. It must not be a term requiring any kind of further evaluation to get a value, such as would be the case for identifiers or function applications.
type_to_construct	The type which the constructed expr returned is expected to have. This type must be compatible with the sort of value_term.
ns	The namespace to resolve c_enum_tag_type to reconstruct the correct type of enum values in the trace.

Note

The type is required separately in order to carry out this conversion, because the smt value term does not contain all the required information. For example an 8 bit, bit vector with a value of 255 could be used to construct an unsigned char with the value 255 or alternatively a signed char with the value -1. So these alternatives are disambiguated using the type.

Definition at line 136 of file construct_value_expr_from_smt.cpp.