CBMC
|
#include <expr2c_class.h>
Public Member Functions | |
expr2ct (const namespacet &_ns, const expr2c_configurationt &configuration=expr2c_configurationt::default_configuration) | |
virtual | ~expr2ct () |
virtual std::string | convert (const typet &src) |
virtual std::string | convert (const exprt &src) |
void | get_shorthands (const exprt &expr) |
std::string | convert_with_identifier (const typet &src, const std::string &identifier) |
Build a declaration string, which requires converting both a type and putting an identifier in the syntactically correct position. | |
Static Protected Member Functions | |
static std::string | indent_str (unsigned indent) |
Protected Attributes | |
const namespacet & | ns |
const expr2c_configurationt & | configuration |
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > | ns_collision |
std::unordered_map< irep_idt, irep_idt > | shorthands |
unsigned | sizeof_nesting |
Definition at line 34 of file expr2c_class.h.
|
inlineexplicit |
Definition at line 37 of file expr2c_class.h.
|
inlinevirtual |
Definition at line 44 of file expr2c_class.h.
Reimplemented in expr2javat.
Definition at line 4172 of file expr2c.cpp.
Reimplemented in expr2javat.
Definition at line 213 of file expr2c.cpp.
Definition at line 1154 of file expr2c.cpp.
|
protectedvirtual |
Definition at line 2052 of file expr2c.cpp.
Definition at line 2228 of file expr2c.cpp.
Definition at line 2331 of file expr2c.cpp.
|
protected |
Definition at line 1614 of file expr2c.cpp.
Definition at line 1334 of file expr2c.cpp.
|
protectedvirtual |
To generate a C-like type declaration of an array.
Includes the size of the array in the []
src | The array type to convert |
qualifiers | Any qualifiers on the type |
declarator_str | Previously computed string denoting the array symbol |
Definition at line 726 of file expr2c.cpp.
|
protected |
To generate a C-like type declaration of an array.
Optionally can include or exclude the size of the array in the []
src | The array type to convert |
qualifiers | Any qualifiers on the type |
declarator_str | Previously computed string denoting the array symbol |
inc_size_if_possible | Should the generated string include the size of the array (if it is known). |
Definition at line 743 of file expr2c.cpp.
|
protected |
Definition at line 1034 of file expr2c.cpp.
|
protected |
Definition at line 846 of file expr2c.cpp.
|
protected |
Definition at line 3588 of file expr2c.cpp.
|
protected |
Definition at line 1344 of file expr2c.cpp.
|
protected |
Definition at line 1370 of file expr2c.cpp.
Definition at line 3468 of file expr2c.cpp.
Reimplemented in expr2javat, and expr2cppt.
Definition at line 3006 of file expr2c.cpp.
Definition at line 3350 of file expr2c.cpp.
Definition at line 3372 of file expr2c.cpp.
Definition at line 3328 of file expr2c.cpp.
Definition at line 2587 of file expr2c.cpp.
Definition at line 3393 of file expr2c.cpp.
Definition at line 3406 of file expr2c.cpp.
|
protected |
Definition at line 2946 of file expr2c.cpp.
|
protected |
Definition at line 2790 of file expr2c.cpp.
|
protected |
Definition at line 2842 of file expr2c.cpp.
Definition at line 2895 of file expr2c.cpp.
Definition at line 2969 of file expr2c.cpp.
|
protected |
Definition at line 2691 of file expr2c.cpp.
Definition at line 2984 of file expr2c.cpp.
Definition at line 3255 of file expr2c.cpp.
Definition at line 2909 of file expr2c.cpp.
|
protected |
Definition at line 3151 of file expr2c.cpp.
Definition at line 2852 of file expr2c.cpp.
|
protected |
Definition at line 3185 of file expr2c.cpp.
Definition at line 2778 of file expr2c.cpp.
|
protected |
Definition at line 2720 of file expr2c.cpp.
Definition at line 3285 of file expr2c.cpp.
|
protected |
Definition at line 3420 of file expr2c.cpp.
Definition at line 3159 of file expr2c.cpp.
Definition at line 3307 of file expr2c.cpp.
Definition at line 3233 of file expr2c.cpp.
Definition at line 2757 of file expr2c.cpp.
Definition at line 2799 of file expr2c.cpp.
|
protected |
Definition at line 3438 of file expr2c.cpp.
Definition at line 3172 of file expr2c.cpp.
|
protected |
Definition at line 2665 of file expr2c.cpp.
Definition at line 1260 of file expr2c.cpp.
Definition at line 1284 of file expr2c.cpp.
Definition at line 1000 of file expr2c.cpp.
Definition at line 3563 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2javat, and expr2cppt.
Definition at line 1790 of file expr2c.cpp.
|
protectedvirtual |
To get the C-like representation of a given boolean value.
boolean_value | The value of the constant bool expression |
Definition at line 2065 of file expr2c.cpp.
Definition at line 2451 of file expr2c.cpp.
|
protected |
Definition at line 3517 of file expr2c.cpp.
|
protected |
Definition at line 3528 of file expr2c.cpp.
Returns a string if src
is a function with a known conversion, else returns nullopt.
Definition at line 4115 of file expr2c.cpp.
Definition at line 1239 of file expr2c.cpp.
|
protected |
Definition at line 2494 of file expr2c.cpp.
Definition at line 3473 of file expr2c.cpp.
|
protected |
Definition at line 1417 of file expr2c.cpp.
Definition at line 1522 of file expr2c.cpp.
Definition at line 2365 of file expr2c.cpp.
Definition at line 935 of file expr2c.cpp.
Definition at line 1223 of file expr2c.cpp.
|
protected |
Definition at line 1532 of file expr2c.cpp.
Definition at line 1512 of file expr2c.cpp.
|
protected |
Definition at line 1086 of file expr2c.cpp.
Definition at line 1188 of file expr2c.cpp.
|
protected |
Definition at line 1715 of file expr2c.cpp.
|
protected |
Definition at line 1685 of file expr2c.cpp.
Definition at line 1634 of file expr2c.cpp.
|
protected |
Definition at line 1720 of file expr2c.cpp.
Definition at line 2551 of file expr2c.cpp.
|
protected |
Definition at line 1436 of file expr2c.cpp.
|
protected |
Definition at line 1473 of file expr2c.cpp.
|
protected |
Definition at line 3642 of file expr2c.cpp.
Definition at line 1697 of file expr2c.cpp.
Definition at line 1703 of file expr2c.cpp.
Definition at line 1691 of file expr2c.cpp.
Definition at line 1213 of file expr2c.cpp.
Definition at line 1228 of file expr2c.cpp.
|
protected |
Definition at line 3660 of file expr2c.cpp.
|
protected |
Definition at line 3623 of file expr2c.cpp.
Definition at line 1709 of file expr2c.cpp.
|
protected |
Definition at line 3604 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2javat, and expr2cppt.
Definition at line 218 of file expr2c.cpp.
|
protected |
Conversion function from rol/ror expressions to C code strings Note that this constructs a complex expression to do bit twiddling since rol/ror operations are not native to ANSI-C.
The complex expression is then recursively converted.
src | is an exprt that must be either an rol or ror |
precedence | precedence for bracketing |
Definition at line 2391 of file expr2c.cpp.
|
protected |
Definition at line 2522 of file expr2c.cpp.
Definition at line 3549 of file expr2c.cpp.
|
protected |
Definition at line 1198 of file expr2c.cpp.
Reimplemented in expr2javat, and expr2cppt.
Definition at line 2073 of file expr2c.cpp.
|
protected |
To generate a C-like string representing a struct.
Can optionally include the padding parameters.
src | The struct declaration expression | |
[out] | precedence | Precedence of the top level operator in the resulting string, used to decide about adding parentheses |
include_padding_components | Should the generated C code include the padding members added to structs for GOTOs benefit |
Definition at line 2089 of file expr2c.cpp.
|
protected |
Definition at line 1624 of file expr2c.cpp.
|
protected |
To generate C-like string for declaring (or defining) the given struct.
src | the struct type being converted |
qualifiers | any qualifiers on the type |
declarator | the declarator on the type |
inc_struct_body | when generating the code, should we include a complete definition of the struct |
inc_padding_components | should the padding parameters be included Note this only makes sense if inc_struct_body |
Definition at line 673 of file expr2c.cpp.
|
protectedvirtual |
To generate C-like string for defining the given struct.
src | the struct type being converted |
qualifiers_str | any qualifiers on the type |
declarator_str | the declarator on the type |
Definition at line 650 of file expr2c.cpp.
Definition at line 1645 of file expr2c.cpp.
|
protected |
Definition at line 799 of file expr2c.cpp.
|
protected |
Definition at line 765 of file expr2c.cpp.
|
protected |
Definition at line 1134 of file expr2c.cpp.
|
protected |
Definition at line 1395 of file expr2c.cpp.
Definition at line 2209 of file expr2c.cpp.
|
protected |
Definition at line 962 of file expr2c.cpp.
Definition at line 2162 of file expr2c.cpp.
Definition at line 869 of file expr2c.cpp.
Build a declaration string, which requires converting both a type and putting an identifier in the syntactically correct position.
src | the type to convert |
identifier | the identifier to use as the type |
Definition at line 4183 of file expr2c.cpp.
|
protectedvirtual |
Reimplemented in expr2javat, and expr2cppt.
Definition at line 3680 of file expr2c.cpp.
Definition at line 116 of file expr2c.cpp.
Definition at line 75 of file expr2c.cpp.
|
staticprotected |
Definition at line 2582 of file expr2c.cpp.
|
protected |
Definition at line 56 of file expr2c_class.h.
|
protected |
Definition at line 55 of file expr2c_class.h.
Definition at line 88 of file expr2c_class.h.
Definition at line 89 of file expr2c_class.h.
|
protected |
Definition at line 91 of file expr2c_class.h.