CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
expr2c.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
15class exprt;
16class namespacet;
17class typet;
18
77
78std::string expr2c(const exprt &expr, const namespacet &ns);
79
80std::string expr2c(
81 const exprt &expr,
82 const namespacet &ns,
83 const expr2c_configurationt &configuration);
84
85std::string type2c(const typet &type, const namespacet &ns);
86
87std::string type2c(
88 const typet &type,
89 const namespacet &ns,
90 const expr2c_configurationt &configuration);
91
92std::string type2c(
93 const typet &type,
94 const std::string &identifier,
95 const namespacet &ns,
96 const expr2c_configurationt &configuration);
97
98#endif // CPROVER_ANSI_C_EXPR2C_H
Base class for all expressions.
Definition expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The type of an expression, extends irept.
Definition type.h:29
std::string type2c(const typet &type, const namespacet &ns)
Definition expr2c.cpp:4181
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition expr2c.cpp:4166
Used for configuring the behaviour of expr2c and type2c.
Definition expr2c.h:21
bool print_enum_int_value
When printing an enum-typed constant, print the integer representation.
Definition expr2c.h:43
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Definition expr2c.h:52
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, const bool print_enum_int_value, const bool expand_typedef)
Definition expr2c.h:49
bool expand_typedef
Print the expanded type instead of a typedef name, even when a typedef is present.
Definition expr2c.h:47
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:40
std::string true_string
This is the string that will be printed for the true boolean expression.
Definition expr2c.h:34
bool print_struct_body_in_type
When printing a struct_typet, should the components of the struct be printed inline.
Definition expr2c.h:28
bool use_library_macros
This is the string that will be printed for null pointers.
Definition expr2c.h:40
bool include_struct_padding_components
When printing struct_typet or struct_exprt, include the artificial padding components introduced to k...
Definition expr2c.h:24
std::string false_string
This is the string that will be printed for the false boolean expression.
Definition expr2c.h:37
bool include_array_size
When printing array_typet, should the size of the array be printed.
Definition expr2c.h:31