9 #ifndef CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
10 #define CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
132 const std::vector<exprt> &operands,
133 const char operation);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Class for saving the internal state of the conversion process.
void convert_multiary_bool(std::vector< exprt > &operands, const char operation)
Iterates through all the given operands and converts them depending on the operation.
void convert_bool_operand(const exprt &op)
Converts a single boolean operand and introduces an additional nesting layer if needed.
std::string convert(const exprt &expr)
Invokes the conversion process for the given expression and calls itself recursively in the process.
void convert_multiary_bool_operands(const std::vector< exprt > &operands, const char operation)
Iterates through all the given operands and converts them depending on the operation.
void convert_first_non_trivial_operand(std::vector< exprt > &operands)
Iterates through all the given operands in search for the first non-trivial operand (that encloses al...
bool is_reference
Flag to specify if the next symbol to convert is a reference to a variable.
expr2stlt(const namespacet &ns)
Creates a new instance of the converter.
const namespacet & ns
Contains the symbol table of the current program to convert.
irep_idt id_shorthand(const irep_idt &identifier)
Returns the given identifier in a form that is compatible with STL by looking up the symbol or cuttin...
std::stringstream result
Used for saving intermediate results of the conversion process.
bool inside_bit_string
Internal representation of the FC bit in STL.
Base class for all expressions.
typet & type()
Return the type of the expression.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a symbol (variable)
The type of an expression, extends irept.
std::string expr2stl(const exprt &expr, const namespacet &ns)
Converts a given expression to human-readable STL code.
std::string type2stl(const typet &type, const namespacet &ns)
Converts a given type to human-readable STL code.