cprover
expr2c.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_ANSI_C_EXPR2C_H
11 #define CPROVER_ANSI_C_EXPR2C_H
12 
13 #include <string>
14 
15 class exprt;
16 class namespacet;
17 class typet;
18 
21 {
25 
29 
32 
34  std::string true_string;
35 
37  std::string false_string;
38 
41 
44  const bool print_struct_body_in_type,
45  const bool include_array_size,
46  const std::string &true_string,
47  const std::string &false_string,
48  const bool use_library_macros)
55  {
56  }
57 
61 
65 };
66 
67 std::string expr2c(const exprt &expr, const namespacet &ns);
68 
69 std::string expr2c(
70  const exprt &expr,
71  const namespacet &ns,
72  const expr2c_configurationt &configuration);
73 
74 std::string type2c(const typet &type, const namespacet &ns);
75 
76 std::string type2c(
77  const typet &type,
78  const namespacet &ns,
79  const expr2c_configurationt &configuration);
80 
81 std::string type2c(
82  const typet &type,
83  const std::string &identifier,
84  const namespacet &ns,
85  const expr2c_configurationt &configuration);
86 
87 #endif // CPROVER_ANSI_C_EXPR2C_H
typet
The type of an expression, extends irept.
Definition: type.h:29
expr2c_configurationt::use_library_macros
bool use_library_macros
This is the string that will be printed for null pointers.
Definition: expr2c.h:40
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition: expr2c.cpp:3889
exprt
Base class for all expressions.
Definition: expr.h:53
expr2c_configurationt::default_configuration
static expr2c_configurationt default_configuration
This prints a human readable C like syntax that closely mirrors the internals of the GOTO program.
Definition: expr2c.h:60
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
type2c
std::string type2c(const typet &type, const namespacet &ns)
Definition: expr2c.cpp:3904
expr2c_configurationt::include_struct_padding_components
bool include_struct_padding_components
When printing struct_typet or struct_exprt, include the artificial padding components introduced to k...
Definition: expr2c.h:24
expr2c_configurationt::print_struct_body_in_type
bool print_struct_body_in_type
When printing a struct_typet, should the components of the struct be printed inline.
Definition: expr2c.h:28
expr2c_configurationt::clean_configuration
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Definition: expr2c.h:64
expr2c_configurationt::include_array_size
bool include_array_size
When printing array_typet, should the size of the array be printed.
Definition: expr2c.h:31
expr2c_configurationt::expr2c_configurationt
expr2c_configurationt(const bool include_struct_padding_components, const bool print_struct_body_in_type, const bool include_array_size, const std::string &true_string, const std::string &false_string, const bool use_library_macros)
Definition: expr2c.h:42
expr2c_configurationt
Used for configuring the behaviour of expr2c and type2c.
Definition: expr2c.h:21
expr2c_configurationt::true_string
std::string true_string
This is the string that will be printed for the true boolean expression.
Definition: expr2c.h:34
expr2c_configurationt::false_string
std::string false_string
This is the string that will be printed for the false boolean expression.
Definition: expr2c.h:37