80 if(!
ns.lookup(identifier, symbol) &&
87 std::string::size_type
pos=
sh.rfind(
"::");
88 if(
pos!=std::string::npos)
98 std::string::size_type
c_pos=dest.find(
"::");
99 if(
c_pos!=std::string::npos &&
100 dest.rfind(
"::")==
c_pos)
101 dest.erase(0,
c_pos+2);
102 else if(
c_pos!=std::string::npos)
112 std::replace(dest.begin(), dest.end(),
'.',
'_');
193 const auto params =
func_type.parameters();
194 for(
const auto &
param : params)
222 const std::string &declarator)
224 std::unique_ptr<qualifierst> clone =
qualifiers.clone();
230 std::string d = declarator.empty() ? declarator :
" " + declarator;
273 return q+
"long double"+d;
276 std::string
swidth = std::to_string(width);
286 return q +
CPROVER_PREFIX +
"fixedbv[" + std::to_string(width) +
"][" +
306 return q+
"signed char"+d;
308 return q+
"unsigned char"+d;
369 std::string dest=
q+
"union";
425 for(c_enum_typet::memberst::const_iterator it = members.begin();
431 if(it != members.begin())
434 result +=
id2string(it->get_base_name());
449 std::string result=
q+
"enum";
463 if(!
q.empty() && (!declarator.empty() || base_type.
id() ==
ID_pointer))
489 std::string dest=
q+
"struct";
502 std::string dest=
q+
"union";
516 std::string dest=declarator+
"(";
520 if(parameters.empty())
527 for(code_typet::parameterst::const_iterator
528 it=parameters.begin();
529 it!=parameters.end();
532 if(it!=parameters.begin())
535 if(it->get_identifier().empty())
578 if(dest[dest.size()-1]==
' ')
579 dest.resize(dest.size()-1);
593 if(
tmp==
"signed char" ||
tmp==
"char")
595 else if(
tmp==
"signed short int")
597 else if(
tmp==
"signed int")
599 else if(
tmp==
"signed long long int")
601 else if(
tmp==
"float")
603 else if(
tmp==
"double")
609 dest+=
" __attribute__((vector_size (";
611 dest+=
"*sizeof("+subtype+
"))))";
619 return q+
"__attribute__(("+
id2string(src.
id())+
")) void"+d;
664 const std::string &declarator,
775 std::string dest =
"(" +
convert(to_type) +
")";
838 const std::string &symbol,
850 std::string dest=symbol+
" { ";
880 for(
size_t i=1; i<src.
operands().size(); i+=2)
882 std::string op1, op2;
893 const typet &full_type =
ns.follow(old.type());
931 std::string dest =
"LET ";
935 const auto &values = src.
values();
960 std::string op0, op1, op2;
974 const exprt &designator = src.
op1();
976 for(
const auto &op : designator.
operands())
1001 std::string dest=
"cond {\n";
1018 condition=!condition;
1028 const std::string &symbol,
1080 const std::string &symbol,
1128 const std::string &symbol,
1134 std::string dest=symbol;
1157 std::string dest =
"ALLOCATE";
1168 dest += op0 +
", " + op1;
1219 return "PROB_UNIFORM(" +
convert(src.
type()) +
"," +
1227 std::string dest=name;
1255 if(*op0.rbegin()==
';')
1256 op0.resize(op0.size()-1);
1260 if(*op1.rbegin()==
';')
1261 op1.resize(op1.size()-1);
1263 std::string dest=op0;
1301 std::string dest=name;
1383 const std::string &symbol,
1428 std::string dest=
"POINTER_ARITHMETIC(";
1467 std::string dest=
"POINTER_DIFFERENCE(";
1522 const auto &compound = src.
compound();
1554 const typet &full_type =
ns.follow(compound.type());
1565 if(!component_name.
empty())
1636 std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
1672 return "ps("+
id+
")";
1678 return "pns("+
id+
")";
1684 return "pps("+
id+
")";
1695 return "nondet_bool()";
1705 std::string result=
"<";
1746 "sizeof value does not fit size_type");
1798 for(
const auto &member : members)
1800 if(member.get_value() == value)
1801 return "/*enum*/" +
id2string(member.get_base_name());
1914 if(!dest.empty() &&
isdigit(dest[dest.size() - 1]))
1916 if(dest.find(
'.')==std::string::npos)
1926 else if(dest.size()==4 &&
1927 (dest[0]==
'+' || dest[0]==
'-'))
1933 else if(dest ==
"-inf")
1935 else if(dest ==
"+NaN")
1937 else if(dest ==
"-NaN")
1943 std::string suffix =
"";
1954 dest =
"(1.0" + suffix +
"/0.0" + suffix +
")";
1955 else if(dest ==
"-inf")
1956 dest =
"(-1.0" + suffix +
"/0.0" + suffix +
")";
1957 else if(dest ==
"+NaN")
1958 dest =
"(0.0" + suffix +
"/0.0" + suffix +
")";
1959 else if(dest ==
"-NaN")
1960 dest =
"(-0.0" + suffix +
"/0.0" + suffix +
")";
1968 if(!dest.empty() &&
isdigit(dest[dest.size() - 1]))
1989 dest=
"(("+
convert(type)+
")"+dest+
")";
1993 value ==
"NULL+offset")
2067 if(components.size()!=src.
operands().size())
2070 std::string dest=
"{ ";
2072 exprt::operandst::const_iterator
o_it=src.
operands().begin();
2081 o_it->type().id() !=
ID_code,
"struct member must not be of code type");
2133 std::string dest=
"{ ";
2139 for(
const auto &op : src.
operands())
2175 std::string dest=
"{ ";
2201 for(
const auto &op : src.
operands())
2203 if(!op.is_constant())
2218 dest.reserve(dest.size()+1+src.
operands().size());
2241 case '\n': dest+=
"\\n";
break;
2242 case '\t': dest+=
"\\t";
break;
2243 case '\v': dest+=
"\\v";
break;
2244 case '\b': dest+=
"\\b";
break;
2245 case '\r': dest+=
"\\r";
break;
2246 case '\f': dest+=
"\\f";
break;
2247 case '\a': dest+=
"\\a";
break;
2248 case '\\': dest+=
"\\\\";
break;
2249 case '"': dest+=
"\\\"";
break;
2252 if(
ch>=
' ' &&
ch!=127 &&
ch<0xff)
2253 dest+=
static_cast<char>(
ch);
2256 std::ostringstream
oss;
2257 oss <<
"\\x" << std::hex <<
ch;
2275 if(it->is_not_nil())
2297 std::string dest=
"{ ";
2424 if(designator.
operands().size() != 1)
2519 std::string dest=
"overflow(\"";
2520 dest+=src.
id().c_str()+9;
2529 for(
const auto &op : src.
operands())
2546 return std::string(indent,
' ');
2561 if(!src.
operands()[1].operands().empty() ||
2562 !src.
operands()[2].operands().empty() ||
2563 !src.
operands()[3].operands().empty() ||
2564 !src.
operands()[4].operands().empty())
2572 if(it->operands().size()==2)
2587 if(it->operands().size()==2)
2640 if(src.
body().is_nil())
2647 src.
body().get_statement()==
ID_block ? indent : indent+2);
2665 if(src.
body().is_nil())
2672 src.
body().get_statement()==
ID_block ? indent : indent+2);
2783 const exprt &op=*it;
2828 const symbolt *symbol=
nullptr;
2839 dest +=
"__declspec(dllexport) ";
2884 if(!src.
init().is_nil())
2889 if(!src.
cond().is_nil())
2892 if(!src.
iter().is_nil())
2895 if(src.
body().is_nil())
2902 src.
body().get_statement()==
ID_block ? indent : indent+2);
2915 for(
const auto &statement : src.
statements())
2917 if(statement.get_statement() ==
ID_label)
2937 for(
const auto &op : src.
operands())
2962 if(dest.empty() || *dest.rbegin()!=
';')
2987 std::ostringstream
oss;
2995 [](
const std::pair<irep_idt, irept> &p) { return p.first; });
3075 if(statement==
"lock")
3078 if(statement==
"unlock")
3184 if(it!=arguments.begin())
3199 std::string dest=
indent_str(indent)+
"printf(";
3221 std::string dest=
indent_str(indent)+
"FENCE(";
3230 for(
unsigned i=0; !
att[i].empty(); i++)
3251 std::string dest=
indent_str(indent)+
"INPUT(";
3273 std::string dest=
indent_str(indent)+
"OUTPUT(";
3294 std::string dest=
indent_str(indent)+
"ARRAY_SET(";
3316 std::string dest=
indent_str(indent)+
"ARRAY_COPY(";
3338 std::string dest=
indent_str(indent)+
"ARRAY_REPLACE(";
3447 std::string dest=
"\n";
3509 std::string dest=
"sizeof(";
3520 const auto &cond = src.
operands().front();
3527 const auto &targets = src.
operands()[1];
3532 if(it != targets.operands().begin())
3545 const std::size_t width =
type_ptr->get_width();
3546 if(width == 8 || width == 16 || width == 32 || width == 64)
3549 src,
"__builtin_bitreverse" + std::to_string(width));
3559 std::string dest = src.
id() ==
ID_r_ok ?
"R_OK"
3655 std::string dest=
"FLOAT_TYPECAST(";
3700 else if(src.
id()==
"pointer_arithmetic")
3703 else if(src.
id()==
"pointer_difference")
3707 return "NULL-object";
3717 else if(src.
id()==
"builtin-function")
3756 pointer.id() ==
ID_plus && pointer.operands().size() == 2 &&
3772 else if(src.
id()==
"array-member-value")
3775 else if(src.
id()==
"struct-member-value")
3823 else if(statement==
"prob_coin")
3825 else if(statement==
"prob_unif")
3935 else if(src.
id()==
"quant_symbol")
3944 else if(src.
id()==
"Hoare")
4072 {
"buffer_size",
"BUFFER_SIZE"},
4073 {
"is_zero_string",
"IS_ZERO_STRING"},
4074 {
"object_value",
"OBJECT_VALUE"},
4075 {
"pointer_base",
"POINTER_BASE"},
4076 {
"pointer_cons",
"POINTER_CONS"},
4077 {
"zero_string",
"ZERO_STRING"},
4078 {
"zero_string_length",
"ZERO_STRING_LENGTH"},
4139 const std::string &identifier)
4151 expr2c.get_shorthands(expr);
4152 return expr2c.convert(expr);
4167 return expr2c.convert(type);
4177 const std::string &identifier,
4182 return expr2c.convert_with_identifier(type, identifier);
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::string MetaString(const std::string &in)
floatbv_typet float_type()
unsignedbv_typet unsigned_int_type()
unsignedbv_typet size_type()
std::string c_type_as_string(const irep_idt &c_type)
signedbv_typet signed_int_type()
bitvector_typet char_type()
bitvector_typet wchar_t_type()
floatbv_typet long_double_type()
floatbv_typet double_type()
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
exprt & symbolic_pointer()
A base class for binary expressions.
A base class for variable bindings (quantifiers, let, lambda)
Reverse the order of bits in a bit-vector.
std::size_t get_width() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
C enum tag type, i.e., c_enum_typet with an identifier.
std::vector< c_enum_membert > memberst
codet representation of an inline assembler statement.
const irep_idt & get_flavor() const
A codet representing sequential composition of program statements.
code_operandst & statements()
codet representation of a do while statement.
const codet & body() const
const exprt & cond() const
codet representation of a for statement.
const exprt & cond() const
const exprt & iter() const
const codet & body() const
const exprt & init() const
A codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
codet representation of an if-then-else statement.
const exprt & cond() const
const codet & else_case() const
const codet & then_case() const
codet representation of a label for branch targets.
const irep_idt & get_label() const
codet representation of a switch-case, i.e. a case statement within a switch.
const exprt & case_op() const
std::vector< parametert > parameterst
codet representing a while statement.
const exprt & cond() const
const codet & body() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string convert_nondet(const exprt &src, unsigned &precedence)
std::string convert_literal(const exprt &src)
std::string convert_code_continue(unsigned indent)
virtual std::string convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str)
To generate a C-like type declaration of an array.
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
std::string convert_comma(const exprt &src, unsigned precedence)
std::string convert_code_assert(const codet &src, unsigned indent)
std::string convert_union(const exprt &src, unsigned &precedence)
std::string convert_code_expression(const codet &src, unsigned indent)
std::string convert_code_goto(const codet &src, unsigned indent)
std::string convert_code_switch(const codet &src, unsigned indent)
std::string convert_pointer_in_range(const pointer_in_range_exprt &src)
std::string convert_initializer_list(const exprt &src)
std::string convert_quantified_symbol(const exprt &src)
std::string convert_binding(const binding_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_function_application(const function_application_exprt &src)
std::string convert_code_unlock(const codet &src, unsigned indent)
std::string convert_code_decl_block(const codet &src, unsigned indent)
static std::string indent_str(unsigned indent)
std::string convert_byte_update(const byte_update_exprt &, unsigned precedence)
std::string convert_code(const codet &src)
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
std::string convert_let(const let_exprt &, unsigned precedence)
std::string convert_nondet_bool()
std::string convert_norep(const exprt &src, unsigned &precedence)
const expr2c_configurationt & configuration
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
std::string convert_code_output(const codet &src, unsigned indent)
std::string convert_code_while(const code_whilet &src, unsigned indent)
std::string convert_index_designator(const exprt &src)
std::string convert_code_frontend_decl(const codet &, unsigned indent)
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
std::string convert_code_block(const code_blockt &src, unsigned indent)
std::string convert_code_asm(const code_asmt &src, unsigned indent)
std::string convert_prophecy_pointer_in_range(const prophecy_pointer_in_range_exprt &src)
std::string convert_allocate(const exprt &src, unsigned &precedence)
std::string convert_Hoare(const exprt &src)
std::string convert_sizeof(const exprt &src, unsigned &precedence)
std::string convert_code_lock(const codet &src, unsigned indent)
std::string convert_r_or_w_ok(const r_or_w_ok_exprt &src)
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
irep_idt id_shorthand(const irep_idt &identifier) const
std::string convert_cond(const exprt &src, unsigned precedence)
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src)
std::string convert_overflow(const exprt &src, unsigned &precedence)
std::string convert_member(const member_exprt &src, unsigned precedence)
void get_shorthands(const exprt &expr)
std::string convert_code_for(const code_fort &src, unsigned indent)
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 sy...
std::string convert_extractbits(const extractbits_exprt &src, unsigned precedence)
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
optionalt< std::string > convert_function(const exprt &src)
Returns a string if src is a function with a known conversion, else returns nullopt.
std::string convert_trinary(const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
std::string convert_update(const update_exprt &, unsigned precedence)
std::string convert_nondet_symbol(const nondet_symbol_exprt &)
std::string convert_code_printf(const codet &src, unsigned indent)
std::string convert_unary(const unary_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
std::string convert_index(const binary_exprt &, unsigned precedence)
std::string convert_member_designator(const exprt &src)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
std::string convert_code_label(const code_labelt &src, unsigned indent)
virtual std::string convert_symbol(const exprt &src)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
std::string convert_code_array_copy(const codet &src, unsigned indent)
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
std::string convert_code_dead(const codet &src, unsigned indent)
virtual std::string convert_annotated_pointer_constant(const annotated_pointer_constant_exprt &src, unsigned &precedence)
std::string convert_rox(const shift_exprt &src, unsigned precedence)
Conversion function from rol/ror expressions to C code strings Note that this constructs a complex ex...
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
std::string convert_designated_initializer(const exprt &src)
std::string convert_vector(const exprt &src, unsigned &precedence)
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string convert_array_member_value(const exprt &src, unsigned precedence)
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
std::unordered_map< irep_idt, irep_idt > shorthands
std::string convert_complex(const exprt &src, unsigned precedence)
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
std::string convert_code_fence(const codet &src, unsigned indent)
std::string convert_bitreverse(const bitreverse_exprt &src)
virtual std::string convert(const typet &src)
std::string convert_code_return(const codet &src, unsigned indent)
std::string convert_code_break(unsigned indent)
virtual std::string convert_struct_type(const typet &src, const std::string &qualifiers_str, const std::string &declarator_str)
To generate C-like string for defining the given struct.
std::string convert_with(const exprt &src, unsigned precedence)
std::string convert_code_frontend_assign(const code_frontend_assignt &, unsigned indent)
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
std::string convert_predicate_passive_symbol(const exprt &src)
std::string convert_array_list(const exprt &src, unsigned &precedence)
std::string convert_array_of(const exprt &src, unsigned precedence)
std::string convert_code_array_replace(const codet &src, unsigned indent)
std::string convert_conditional_target_group(const exprt &src)
std::string convert_code_assume(const codet &src, unsigned indent)
std::string convert_code_input(const codet &src, unsigned indent)
std::string convert_extractbit(const extractbit_exprt &, unsigned precedence)
std::string convert_predicate_next_symbol(const exprt &src)
std::string convert_code_array_set(const codet &src, unsigned indent)
std::string convert_binary(const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
std::string convert_predicate_symbol(const exprt &src)
std::string convert_prophecy_r_or_w_ok(const prophecy_r_or_w_ok_exprt &src)
std::string convert_array(const exprt &src)
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
std::string to_ansi_c_string() const
Application of (mathematical) function.
std::string to_ansi_c_string() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const std::string & id_string() const
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
exprt & where()
convenience accessor for binding().where()
Extract member of struct or union.
const exprt & compound() const
irep_idt get_component_name() const
std::size_t get_component_number() const
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Expression to hold a nondeterministic choice.
const irep_idt & get_identifier() const
The plus expression Associativity is not specified.
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...
const exprt & upper_bound() const
const exprt & lower_bound() const
const exprt & pointer() const
pointer_in_range (see pointer_in_range_exprt) with prophecy expressions to encode whether a pointer r...
const exprt & upper_bound() const
const exprt & lower_bound() const
const exprt & pointer() const
A base class for a predicate that indicates that an address range is ok to read or write or both.
const exprt & pointer() const
const exprt & size() const
A base class for a predicate that indicates that an address range is ok to read or write or both.
const exprt & size() const
const exprt & pointer() const
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
const irep_idt & get_function() const
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
Base type for structs and unions.
std::vector< componentt > componentst
Expression to hold a symbol (variable)
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
An expression with three operands.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Generic base class for unary expressions.
A union tag type, i.e., union_typet with an identifier.
Fixed-width bit-vector with unsigned binary interpretation.
Operator to update elements in structs and arrays.
bool has_prefix(const std::string &s, const std::string &prefix)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
static optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
static std::string clean_identifier(const irep_idt &id)
#define forall_operands(it, expr)
#define forall_expr(it, expr)
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
find_symbols_sett find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables.
API to expression classes for floating-point arithmetic.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void irep2lisp(const irept &src, lispexprt &dest)
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)
API to expression classes for Pointers.
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
const prophecy_pointer_in_range_exprt & to_prophecy_pointer_in_range_expr(const exprt &expr)
const pointer_in_range_exprt & to_pointer_in_range_expr(const exprt &expr)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
#define SYMEX_DYNAMIC_PREFIX
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const code_switch_caset & to_code_switch_case(const codet &code)
const code_frontend_returnt & to_code_frontend_return(const codet &code)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const code_dowhilet & to_code_dowhile(const codet &code)
const code_whilet & to_code_while(const codet &code)
const code_labelt & to_code_label(const codet &code)
const code_blockt & to_code_block(const codet &code)
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const code_frontend_assignt & to_code_frontend_assign(const codet &code)
code_asmt & to_code_asm(codet &code)
const code_fort & to_code_for(const codet &code)
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const string_constantt & to_string_constant(const exprt &expr)
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Used for configuring the behaviour of expr2c and type2c.
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
static expr2c_configurationt default_configuration
This prints a human readable C like syntax that closely mirrors the internals of the GOTO program.
bool has_suffix(const std::string &s, const std::string &suffix)
bool is_signed(const typet &t)
Convenience function – is the type signed?