CBMC
construct_value_expr_from_smt.cpp File Reference
+ 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. More...
 

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_termThis 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_constructThe type which the constructed expr returned is expected to have. This type must be compatible with the sort of value_term.
nsThe 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.