CBMC
expr2statement_list.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Conversion from Expression or Type to Statement List Language
4 
5 Author: Matthias Weiss, matthias.weiss@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
10 #define CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
11 
12 #include <util/irep.h>
13 
14 #include <string>
15 
16 class and_exprt;
17 class equal_exprt;
18 class exprt;
19 class namespacet;
20 class notequal_exprt;
21 class not_exprt;
22 class or_exprt;
23 class symbol_exprt;
24 class typet;
25 class xor_exprt;
26 
31 std::string expr2stl(const exprt &expr, const namespacet &ns);
32 
37 std::string type2stl(const typet &type, const namespacet &ns);
38 
40 class expr2stlt
41 {
45 
49 
51  const namespacet &ns;
52 
54  std::stringstream result;
55 
56 public:
59  explicit expr2stlt(const namespacet &ns);
60 
66  std::string convert(const exprt &expr);
67 
68 private:
74  void convert(const and_exprt &expr);
75 
81  void convert(const or_exprt &expr);
82 
88  void convert(const xor_exprt &expr);
89 
96  void convert(const notequal_exprt &expr);
97 
103  void convert(const equal_exprt &expr);
104 
111  void convert(const not_exprt &expr);
112 
117  void convert(const symbol_exprt &expr);
118 
124  void
125  convert_multiary_bool(std::vector<exprt> &operands, const char operation);
126 
132  const std::vector<exprt> &operands,
133  const char operation);
134 
137  void convert_bool_operand(const exprt &op);
138 
145  void convert_first_non_trivial_operand(std::vector<exprt> &operands);
146 
151  irep_idt id_shorthand(const irep_idt &identifier);
152 };
153 
154 #endif // CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
Boolean AND.
Definition: std_expr.h:2125
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Equality.
Definition: std_expr.h:1366
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.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Boolean negation.
Definition: std_expr.h:2332
Disequality.
Definition: std_expr.h:1425
Boolean OR.
Definition: std_expr.h:2233
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The type of an expression, extends irept.
Definition: type.h:29
Boolean XOR.
Definition: std_expr.h:2296
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.