cprover
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 #include <util/namespace.h>
14 #include <util/std_expr.h>
15 
16 #include <string>
17 
22 std::string expr2stl(const exprt &expr, const namespacet &ns);
23 
28 std::string type2stl(const typet &type, const namespacet &ns);
29 
31 class expr2stlt
32 {
36 
40 
42  const namespacet &ns;
43 
45  std::stringstream result;
46 
47 public:
50  explicit expr2stlt(const namespacet &ns);
51 
57  std::string convert(const exprt &expr);
58 
59 private:
65  void convert(const and_exprt &expr);
66 
72  void convert(const or_exprt &expr);
73 
79  void convert(const xor_exprt &expr);
80 
87  void convert(const notequal_exprt &expr);
88 
94  void convert(const equal_exprt &expr);
95 
102  void convert(const not_exprt &expr);
103 
108  void convert(const symbol_exprt &expr);
109 
115  void
116  convert_multiary_bool(std::vector<exprt> &operands, const char operation);
117 
123  const std::vector<exprt> &operands,
124  const char operation);
125 
128  void convert_bool_operand(const exprt &op);
129 
136  void convert_first_non_trivial_operand(std::vector<exprt> &operands);
137 
142  irep_idt id_shorthand(const irep_idt &identifier);
143 };
144 
145 #endif // CPROVER_STATEMENT_LIST_CONVERTERS_EXPR2STATEMENT_LIST_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet
The type of an expression, extends irept.
Definition: type.h:29
type2stl
std::string type2stl(const typet &type, const namespacet &ns)
Converts a given type to human-readable STL code.
Definition: expr2statement_list.cpp:114
xor_exprt
Boolean XOR.
Definition: std_expr.h:2308
expr2stlt
Class for saving the internal state of the conversion process.
Definition: expr2statement_list.h:32
and_exprt
Boolean AND.
Definition: std_expr.h:2137
exprt
Base class for all expressions.
Definition: expr.h:53
expr2stlt::id_shorthand
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...
Definition: expr2statement_list.cpp:290
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
equal_exprt
Equality.
Definition: std_expr.h:1190
notequal_exprt
Disequality.
Definition: std_expr.h:1248
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
expr2stlt::convert
std::string convert(const exprt &expr)
Invokes the conversion process for the given expression and calls itself recursively in the process.
Definition: expr2statement_list.cpp:127
or_exprt
Boolean OR.
Definition: std_expr.h:2245
expr2stlt::ns
const namespacet & ns
Contains the symbol table of the current program to convert.
Definition: expr2statement_list.h:42
expr2stlt::expr2stlt
expr2stlt(const namespacet &ns)
Creates a new instance of the converter.
Definition: expr2statement_list.cpp:122
expr2stl
std::string expr2stl(const exprt &expr, const namespacet &ns)
Converts a given expression to human-readable STL code.
Definition: expr2statement_list.cpp:107
expr2stlt::convert_bool_operand
void convert_bool_operand(const exprt &op)
Converts a single boolean operand and introduces an additional nesting layer if needed.
Definition: expr2statement_list.cpp:248
expr2stlt::convert_multiary_bool_operands
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.
Definition: expr2statement_list.cpp:229
expr2stlt::inside_bit_string
bool inside_bit_string
Internal representation of the FC bit in STL.
Definition: expr2statement_list.h:35
expr2stlt::convert_multiary_bool
void convert_multiary_bool(std::vector< exprt > &operands, const char operation)
Iterates through all the given operands and converts them depending on the operation.
Definition: expr2statement_list.cpp:216
expr2stlt::convert_first_non_trivial_operand
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...
Definition: expr2statement_list.cpp:266
expr2stlt::is_reference
bool is_reference
Flag to specify if the next symbol to convert is a reference to a variable.
Definition: expr2statement_list.h:39
std_expr.h
API to expression classes.
irep.h
expr2stlt::result
std::stringstream result
Used for saving intermediate results of the conversion process.
Definition: expr2statement_list.h:45
not_exprt
Boolean negation.
Definition: std_expr.h:2843