Go to the documentation of this file.
30 #define NOT_POSTFIX 'N'
36 #define OPERAND_SEPARATOR ' '
39 #define LINE_SEPARATOR ";\n"
43 #define NESTING_OPEN_LINE_SEPARATOR "(;\n"
47 #define NESTING_CLOSED_LINE_SEPARATOR ");\n"
50 #define REFERENCE_FLAG '#'
53 #define SCOPE_SEPARATOR "::"
62 static std::vector<exprt>
65 std::vector<exprt> result;
66 if(ID_not != lhs.
id() && ID_not != rhs.
id())
69 result.push_back(lhs);
72 else if(ID_not != lhs.
id() && ID_not == rhs.
id())
75 result.push_back(lhs);
78 else if(ID_not == lhs.
id() && ID_not != rhs.
id())
82 result.push_back(rhs);
88 result.push_back(rhs);
133 if(ID_and == expr.
id())
135 else if(ID_or == expr.
id())
137 else if(ID_xor == expr.
id())
139 else if(ID_notequal == expr.
id())
141 else if(ID_equal == expr.
id())
143 else if(ID_symbol == expr.
id())
145 else if(ID_not == expr.
id() &&
to_not_expr(expr).op().type().
id() == ID_bool)
155 std::vector<exprt> operands = expr.
operands();
161 std::vector<exprt> operands = expr.
operands();
167 std::vector<exprt> operands = expr.
operands();
173 std::vector<exprt> operands = expr.
operands();
179 std::vector<exprt> operands =
190 if(ID_symbol == expr.
op().
id())
217 std::vector<exprt> &operands,
218 const char operation)
230 const std::vector<exprt> &operands,
231 const char operation)
233 for(
const exprt &op : operands)
235 if(ID_not == op.id())
250 if(op.
id() == ID_symbol)
268 exprt non_trivial_op;
269 for(
auto it{begin(operands)}; it != end(operands); ++it)
272 (ID_symbol == it->id()) ||
277 non_trivial_op = *it;
293 std::string shorthand =
id2string(identifier);
300 if(
pos != std::string::npos)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static std::vector< exprt > instrument_equal_operands(const exprt &lhs, const exprt &rhs)
Modifies the parameters of a binary equal expression with the help of its symmetry properties.
#define NOT_POSTFIX
Postfix for any negated boolean instruction.
#define NESTING_CLOSED_LINE_SEPARATOR
Separator for the end of an instruction that closes a nesting layer.
The type of an expression, extends irept.
Class for saving the internal state of the conversion process.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
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...
Expression to hold a symbol (variable)
bool has_suffix(const std::string &s, const std::string &suffix)
#define OPERAND_SEPARATOR
Separator between the instruction code and it's operand.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
std::string convert(const exprt &expr)
Invokes the conversion process for the given expression and calls itself recursively in the process.
#define REFERENCE_FLAG
Prefix for the reference to any variable.
#define SCOPE_SEPARATOR
CBMC-internal separator for variable scopes.
const std::string & id2string(const irep_idt &d)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
#define PRECONDITION(CONDITION)
const namespacet & ns
Contains the symbol table of the current program to convert.
std::string type2stl(const typet &type, const namespacet &ns)
Converts a given type to human-readable STL code.
const irep_idt & get_identifier() const
expr2stlt(const namespacet &ns)
Creates a new instance of the converter.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void convert_bool_operand(const exprt &op)
Converts a single boolean operand and introduces an additional nesting layer if needed.
const irep_idt & id() const
#define LINE_SEPARATOR
Separator between the end of an instruction and the next one.
#define AND
STL code for an AND instruction.
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
#define XOR
STL code for a XOR instruction.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
bool is_reference(const typet &type)
Returns true if the type is a reference.
#define NESTING_OPEN_LINE_SEPARATOR
Separator for the end of an instruction that introduces a new layer of nesting.
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.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
std::string expr2stl(const exprt &expr, const namespacet &ns)
Converts a given expression to human-readable STL code.
bool inside_bit_string
Internal representation of the FC bit in STL.
void convert_multiary_bool(std::vector< exprt > &operands, const char operation)
Iterates through all the given operands and converts them depending on the operation.
#define NOT
STL code for a NOT instruction.
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
#define OR
STL code for an OR instruction.
unsignedbv_typet size_type()
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_boolean() const
Return whether the expression represents a Boolean.
bool is_reference
Flag to specify if the next symbol to convert is a reference to a variable.
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
static bool is_not_bool(const exprt &expr)
Checks if the expression or one of its parameters is not of type bool.
std::stringstream result
Used for saving intermediate results of the conversion process.