cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
20
struct
expr2c_configurationt
final
21
{
24
bool
include_struct_padding_components
;
25
28
bool
print_struct_body_in_type
;
29
31
bool
include_array_size
;
32
34
std::string
true_string
;
35
37
std::string
false_string
;
38
39
/// This is the string that will be printed for null pointers
40
bool
use_library_macros
;
41
43
bool
print_enum_int_value
;
44
47
bool
expand_typedef
;
48
49
expr2c_configurationt
(
50
const
bool
include_struct_padding_components
,
51
const
bool
print_struct_body_in_type
,
52
const
bool
include_array_size
,
53
const
std::string &
true_string
,
54
const
std::string &
false_string
,
55
const
bool
use_library_macros
,
56
const
bool
print_enum_int_value
,
57
const
bool
expand_typedef
)
58
:
include_struct_padding_components
(
include_struct_padding_components
),
59
print_struct_body_in_type
(
print_struct_body_in_type
),
60
include_array_size
(
include_array_size
),
61
true_string
(
true_string
),
62
false_string
(
false_string
),
63
use_library_macros
(
use_library_macros
),
64
print_enum_int_value
(
print_enum_int_value
),
65
expand_typedef
(
expand_typedef
)
66
{
67
}
68
71
static
expr2c_configurationt
default_configuration
;
72
75
static
expr2c_configurationt
clean_configuration
;
76
};
77
78
std::string
expr2c
(
const
exprt
&expr,
const
namespacet
&ns);
79
80
std::string
expr2c
(
81
const
exprt
&expr,
82
const
namespacet
&ns,
83
const
expr2c_configurationt
&configuration);
84
85
std::string
type2c
(
const
typet
&type,
const
namespacet
&ns);
86
87
std::string
type2c
(
88
const
typet
&type,
89
const
namespacet
&ns,
90
const
expr2c_configurationt
&configuration);
91
92
std::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
exprt
Base class for all expressions.
Definition
expr.h:57
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
typet
The type of an expression, extends irept.
Definition
type.h:29
type2c
std::string type2c(const typet &type, const namespacet &ns)
Definition
expr2c.cpp:4224
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition
expr2c.cpp:4209
expr2c_configurationt
Used for configuring the behaviour of expr2c and type2c.
Definition
expr2c.h:21
expr2c_configurationt::print_enum_int_value
bool print_enum_int_value
When printing an enum-typed constant, print the integer representation.
Definition
expr2c.h:43
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:52
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, const bool print_enum_int_value, const bool expand_typedef)
Definition
expr2c.h:49
expr2c_configurationt::expand_typedef
bool expand_typedef
Print the expanded type instead of a typedef name, even when a typedef is present.
Definition
expr2c.h:47
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:40
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::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::use_library_macros
bool use_library_macros
This is the string that will be printed for null pointers.
Definition
expr2c.h:40
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::false_string
std::string false_string
This is the string that will be printed for the false boolean expression.
Definition
expr2c.h:37
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
ansi-c
expr2c.h
Generated by
1.17.0