construct_value_expr_from_smt.h File Reference

#include <util/expr.h>

Include dependency graph for construct_value_expr_from_smt.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
exprt	construct_value_expr_from_smt (const smt_termt &value_term, const typet &type_to_construct)
	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. More...

Function Documentation

construct_value_expr_from_smt()

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

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.

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 115 of file construct_value_expr_from_smt.cpp.