CBMC
|
#include "expr2c.h"
#include "expr2c_class.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/cprover_prefix.h>
#include <util/find_symbols.h>
#include <util/fixedbv.h>
#include <util/floatbv_expr.h>
#include <util/lispexpr.h>
#include <util/lispirep.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/pointer_offset_size.h>
#include <util/prefix.h>
#include <util/string_constant.h>
#include <util/string_utils.h>
#include <util/suffix.h>
#include <util/symbol.h>
#include "c_misc.h"
#include "c_qualifiers.h"
#include <algorithm>
#include <map>
#include <sstream>
Go to the source code of this file.
Functions | |
static std::string | clean_identifier (const irep_idt &id) |
static std::optional< exprt > | build_sizeof_expr (const constant_exprt &expr, const namespacet &ns) |
std::string | expr2c (const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration) |
std::string | expr2c (const exprt &expr, const namespacet &ns) |
std::string | type2c (const typet &type, const namespacet &ns, const expr2c_configurationt &configuration) |
std::string | type2c (const typet &type, const namespacet &ns) |
std::string | type2c (const typet &type, const std::string &identifier, const namespacet &ns, const expr2c_configurationt &configuration) |
|
static |
Definition at line 1726 of file expr2c.cpp.
|
static |
Definition at line 93 of file expr2c.cpp.
std::string expr2c | ( | const exprt & | expr, |
const namespacet & | ns | ||
) |
Definition at line 4166 of file expr2c.cpp.
std::string expr2c | ( | const exprt & | expr, |
const namespacet & | ns, | ||
const expr2c_configurationt & | configuration | ||
) |
Definition at line 4155 of file expr2c.cpp.
std::string type2c | ( | const typet & | type, |
const namespacet & | ns | ||
) |
Definition at line 4181 of file expr2c.cpp.
std::string type2c | ( | const typet & | type, |
const namespacet & | ns, | ||
const expr2c_configurationt & | configuration | ||
) |
Definition at line 4171 of file expr2c.cpp.
std::string type2c | ( | const typet & | type, |
const std::string & | identifier, | ||
const namespacet & | ns, | ||
const expr2c_configurationt & | configuration | ||
) |
Definition at line 4186 of file expr2c.cpp.