79 if(!
ns.lookup(identifier, symbol) &&
86 std::string::size_type
pos=sh.rfind(
"::");
87 if(
pos!=std::string::npos)
97 std::string::size_type c_pos=dest.find(
"::");
98 if(c_pos!=std::string::npos &&
99 dest.rfind(
"::")==c_pos)
100 dest.erase(0, c_pos+2);
101 else if(c_pos!=std::string::npos)
111 std::replace(dest.begin(), dest.end(),
'.',
'_');
121 for(
const auto &symbol_id : symbols)
124 bool is_param = !
ns.lookup(symbol_id, symbol) && symbol->
is_parameter;
132 func = func.substr(0, func.rfind(
"::"));
137 if(!
ns.lookup(sh, global_symbol))
142 if(!
shorthands.insert(std::make_pair(symbol_id, sh)).second)
146 for(
const auto &symbol_id : symbols)
162 has_collision=!
ns.lookup(sh, symbol);
172 if(!
ns.lookup(symbol_id, symbol))
183 const std::string symbol_str =
id2string(symbol_id);
184 const std::string func = symbol_str.substr(0, symbol_str.find(
"::"));
186 if(!
ns.lookup(func, func_symbol))
190 const auto func_type =
192 const auto params = func_type.parameters();
193 for(
const auto ¶m : params)
195 const auto param_id = param.get_identifier();
196 if(param_id != symbol_id && sh ==
id_shorthand(param_id))
198 has_collision =
true;
209 shorthands.insert(std::make_pair(symbol_id, sh));
221 const std::string &declarator)
223 std::unique_ptr<c_qualifierst> clone = qualifiers.
clone();
225 new_qualifiers.
read(src);
227 std::string q=new_qualifiers.
as_string();
229 std::string d = declarator.empty() ? declarator :
" " + declarator;
236 if(src.
id()==ID_bool)
240 else if(src.
id()==ID_c_bool)
244 else if(src.
id()==ID_string)
248 else if(src.
id()==ID_natural ||
249 src.
id()==ID_integer ||
250 src.
id()==ID_rational)
254 else if(src.
id()==ID_empty)
258 else if(src.
id()==ID_complex)
263 else if(src.
id()==ID_floatbv)
267 if(width==
config.ansi_c.single_width)
269 else if(width==
config.ansi_c.double_width)
271 else if(width==
config.ansi_c.long_double_width)
272 return q+
"long double"+d;
275 std::string swidth = std::to_string(width);
277 return q +
CPROVER_PREFIX +
"floatbv[" + swidth +
"][" + fwidth +
"]";
280 else if(src.
id()==ID_fixedbv)
285 return q +
CPROVER_PREFIX +
"fixedbv[" + std::to_string(width) +
"][" +
286 std::to_string(fraction_bits) +
"]" + d;
288 else if(src.
id()==ID_c_bit_field)
294 else if(src.
id()==ID_signedbv ||
295 src.
id()==ID_unsignedbv)
301 if(c_type==ID_char &&
302 config.ansi_c.char_is_unsigned!=(src.
id()==ID_unsignedbv))
304 if(src.
id()==ID_signedbv)
305 return q+
"signed char"+d;
307 return q+
"unsigned char"+d;
309 else if(c_type!=ID_wchar_t && !c_type_str.empty())
310 return q+c_type_str+d;
317 std::string sign_str=
is_signed?
"signed ":
"unsigned ";
319 if(width==
config.ansi_c.int_width)
323 return q+sign_str+
"int"+d;
325 else if(width==
config.ansi_c.long_int_width)
329 return q+sign_str+
"long int"+d;
331 else if(width==
config.ansi_c.char_width)
334 return q+sign_str+
"char"+d;
336 else if(width==
config.ansi_c.short_int_width)
340 return q+sign_str+
"short int"+d;
342 else if(width==
config.ansi_c.long_long_int_width)
346 return q+sign_str+
"long long int"+d;
352 return q + sign_str +
"__int128" + d;
360 else if(src.
id()==ID_struct)
364 else if(src.
id()==ID_union)
368 std::string dest=q+
"union";
392 else if(src.
id()==ID_c_enum)
424 for(c_enum_typet::memberst::const_iterator it = members.begin();
430 if(it != members.begin())
433 result +=
id2string(it->get_base_name());
444 else if(src.
id()==ID_c_enum_tag)
447 const symbolt &symbol=
ns.lookup(c_enum_tag_type);
448 std::string result=q+
"enum";
453 else if(src.
id()==ID_pointer)
457 sub_qualifiers.
read(base_type);
460 std::string new_declarator=
"*";
462 if(!q.empty() && (!declarator.empty() || base_type.
id() == ID_pointer))
464 new_declarator+=
" "+q;
467 new_declarator+=declarator;
471 base_type.
id() == ID_code ||
474 new_declarator=
"("+new_declarator+
")";
477 return convert_rec(base_type, sub_qualifiers, new_declarator);
479 else if(src.
id()==ID_array)
483 else if(src.
id()==ID_struct_tag)
488 std::string dest=q+
"struct";
489 const std::string &tag=
ns.follow_tag(struct_tag_type).get_string(ID_tag);
496 else if(src.
id()==ID_union_tag)
501 std::string dest=q+
"union";
502 const std::string &tag=
ns.follow_tag(union_tag_type).get_string(ID_tag);
509 else if(src.
id()==ID_code)
515 std::string dest=declarator+
"(";
519 if(parameters.empty())
526 for(code_typet::parameterst::const_iterator
527 it=parameters.begin();
528 it!=parameters.end();
531 if(it!=parameters.begin())
534 if(it->get_identifier().empty())
538 std::string arg_declarator=
563 const typet *non_ptr_type = &return_type;
564 while(non_ptr_type->
id()==ID_pointer)
567 if(non_ptr_type->
id()==ID_code ||
568 non_ptr_type->
id()==ID_array)
569 dest=
convert_rec(return_type, ret_qualifiers, dest);
571 dest=
convert_rec(return_type, ret_qualifiers,
"")+
" "+dest;
577 if(dest[dest.size()-1]==
' ')
578 dest.resize(dest.size()-1);
583 else if(src.
id()==ID_vector)
592 if(tmp==
"signed char" || tmp==
"char")
594 else if(tmp==
"signed short int")
596 else if(tmp==
"signed int")
598 else if(tmp==
"signed long long int")
600 else if(tmp==
"float")
602 else if(tmp==
"double")
608 dest+=
" __attribute__((vector_size (";
610 dest+=
"*sizeof("+subtype+
"))))";
615 else if(src.
id()==ID_constructor ||
616 src.
id()==ID_destructor)
618 return q+
"__attribute__(("+
id2string(src.
id())+
")) void"+d;
620 else if(src.
id() == ID_bv)
624 if(c_type == ID_c_signed_bitint)
626 return "_BitInt(" + src.
get_string(ID_C_c_bitint_width) +
")";
628 else if(c_type == ID_c_unsigned_bitint)
630 return "unsigned _BitInt(" + src.
get_string(ID_C_c_bitint_width) +
")";
652 const std::string &qualifiers_str,
653 const std::string &declarator_str)
675 const std::string &qualifiers,
676 const std::string &declarator,
677 bool inc_struct_body,
678 bool inc_padding_components)
684 inc_struct_body || !inc_padding_components,
"inconsistent configuration");
688 std::string dest=qualifiers+
"struct";
701 if(
component.get_is_padding() && !inc_padding_components)
729 const std::string &declarator_str)
732 src, qualifiers, declarator_str,
configuration.include_array_size);
746 const std::string &declarator_str,
747 bool inc_size_if_possible)
750 std::string array_suffix;
752 if(
to_array_type(src).size().is_nil() || !inc_size_if_possible)
762 declarator_str + array_suffix);
767 unsigned &precedence)
777 if(to_type.
id()==ID_c_bool &&
781 if(to_type.
id()==ID_bool &&
785 std::string dest =
"(" +
convert(to_type) +
")";
801 const std::string &symbol1,
802 const std::string &symbol2,
848 const std::string &symbol,
860 std::string dest=symbol+
" { ";
890 for(
size_t i=1; i<src.
operands().size(); i+=2)
892 std::string op1, op2;
898 if(src.
operands()[i].id()==ID_member_name)
901 src.
operands()[i].get(ID_component_name);
904 (old.type().
id() == ID_struct_tag || old.type().id() == ID_union_tag)
906 .get_component(component_name)
913 display_component_name=component_name;
917 op1=
"."+
id2string(display_component_name);
939 std::string dest =
"LET ";
943 const auto &values = src.
values();
944 auto values_it = values.begin();
968 std::string op0, op1, op2;
982 const exprt &designator = src.
op1();
984 for(
const auto &op : designator.
operands())
1002 unsigned precedence)
1007 bool condition=
true;
1009 std::string dest=
"cond {\n";
1011 for(
const auto &operand : src.
operands())
1026 condition=!condition;
1036 const std::string &symbol,
1037 unsigned precedence,
1038 bool full_parentheses)
1057 bool use_parentheses0=
1059 (precedence==p0 && full_parentheses) ||
1060 (precedence==p0 && src.
id()!=op0.
id());
1062 if(use_parentheses0)
1065 if(use_parentheses0)
1072 bool use_parentheses1=
1074 (precedence==p1 && full_parentheses) ||
1075 (precedence==p1 && src.
id()!=op1.
id());
1077 if(use_parentheses1)
1080 if(use_parentheses1)
1088 const std::string &symbol,
1089 unsigned precedence,
1090 bool full_parentheses)
1098 for(
const auto &operand : src.
operands())
1120 bool use_parentheses = precedence > p ||
1121 (precedence == p && full_parentheses) ||
1122 (precedence == p && src.
id() != operand.id());
1136 const std::string &symbol,
1137 unsigned precedence)
1142 std::string dest=symbol;
1165 std::string dest =
"ALLOCATE";
1169 src.
type().
id() == ID_pointer &&
1176 dest += op0 +
", " + op1;
1184 unsigned &precedence)
1194 unsigned &precedence)
1209 unsigned &precedence)
1224 unsigned &precedence)
1227 return "PROB_UNIFORM(" +
convert(src.
type()) +
"," +
1235 std::string dest=name;
1256 unsigned precedence)
1263 if(*op0.rbegin()==
';')
1264 op0.resize(op0.size()-1);
1268 if(*op1.rbegin()==
';')
1269 op1.resize(op1.size()-1);
1271 std::string dest=op0;
1280 unsigned precedence)
1309 std::string dest=name;
1330 unsigned precedence)
1340 unsigned precedence)
1391 const std::string &symbol,
1392 unsigned precedence)
1431 const exprt &src,
unsigned &precedence)
1436 std::string dest=
"POINTER_ARITHMETIC(";
1468 const exprt &src,
unsigned &precedence)
1475 std::string dest=
"POINTER_DIFFERENCE(";
1480 op =
convert(binary_expr.op0().type());
1508 unsigned precedence;
1513 return "."+src.
get_string(ID_component_name);
1518 unsigned precedence;
1528 unsigned precedence)
1530 const auto &compound = src.
compound();
1535 if(compound.id() == ID_dereference)
1541 if(precedence > p || pointer.id() == ID_typecast)
1544 if(precedence > p || pointer.id() == ID_typecast)
1553 if(precedence > p || compound.id() == ID_typecast)
1556 if(precedence > p || compound.id() == ID_typecast)
1563 compound.type().id() != ID_struct && compound.type().id() != ID_union &&
1564 compound.type().id() != ID_struct_tag &&
1565 compound.type().id() != ID_union_tag)
1571 (compound.type().
id() == ID_struct_tag ||
1572 compound.type().id() == ID_union_tag)
1578 if(!component_name.
empty())
1580 const auto &comp_expr = struct_union_type.
get_component(component_name);
1582 if(comp_expr.is_nil())
1585 if(!comp_expr.get_pretty_name().empty())
1586 dest +=
id2string(comp_expr.get_pretty_name());
1598 const auto &comp_expr = struct_union_type.
components()[n];
1600 if(!comp_expr.get_pretty_name().empty())
1601 dest +=
id2string(comp_expr.get_pretty_name());
1603 dest +=
id2string(comp_expr.get_name());
1610 unsigned precedence)
1620 unsigned precedence)
1630 unsigned &precedence)
1646 to_unary_expr(src).op().
id() == ID_predicate_passive_symbol)
1652 std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
1687 const std::string &
id=src.
get_string(ID_identifier);
1688 return "ps("+
id+
")";
1693 const std::string &
id=src.
get_string(ID_identifier);
1694 return "pns("+
id+
")";
1699 const std::string &
id=src.
get_string(ID_identifier);
1700 return "pps("+
id+
")";
1705 const std::string &
id=src.
get_string(ID_identifier);
1711 return "nondet_bool()";
1716 unsigned &precedence)
1721 std::string result=
"<";
1738static std::optional<exprt>
1741 const typet &type =
static_cast<const typet &
>(expr.
find(ID_C_c_sizeof_type));
1747 std::optional<mp_integer> type_size;
1748 if(type_size_expr.has_value())
1753 !type_size.has_value() || *type_size < 0 || !val.has_value() ||
1754 *val < *type_size || (*type_size == 0 && *val > 0))
1762 "sizeof value does not fit size_type");
1768 remainder = *val % *type_size;
1773 exprt result(ID_sizeof, t);
1774 result.
set(ID_type_arg, type);
1786 unsigned &precedence)
1793 if(type.
id()==ID_integer ||
1794 type.
id()==ID_natural ||
1795 type.
id()==ID_rational)
1799 else if(type.
id()==ID_c_enum ||
1800 type.
id()==ID_c_enum_tag)
1806 if(c_enum_type.
id()!=ID_c_enum)
1814 for(
const auto &member : members)
1816 if(member.get_value() == value)
1817 return "/*enum*/" +
id2string(member.get_base_name());
1826 std::string value_as_string =
1830 return value_as_string;
1832 return "/*enum*/" + value_as_string;
1834 else if(type.
id()==ID_rational)
1836 else if(type.
id()==ID_bv)
1840 if(c_type == ID_c_signed_bitint)
1843 auto width = src.
get_int(ID_C_c_bitint_width);
1847 else if(c_type == ID_c_unsigned_bitint)
1850 auto width = src.
get_int(ID_C_c_bitint_width);
1857 else if(type.
id()==ID_bool)
1861 else if(type.
id()==ID_unsignedbv ||
1862 type.
id()==ID_signedbv ||
1863 type.
id()==ID_c_bit_field ||
1864 type.
id()==ID_c_bool)
1871 type.
id() == ID_signedbv ||
1872 (type.
id() == ID_c_bit_field &&
1876 type.
id() == ID_c_bit_field
1878 : type.
get(ID_C_c_type);
1880 if(type.
id()==ID_c_bool)
1890 else if(int_value==
'\r')
1892 else if(int_value==
'\t')
1894 else if(int_value==
'\'')
1896 else if(int_value==
'\\')
1898 else if(int_value>=
' ' && int_value<126)
1918 if(c_type==ID_unsigned_int)
1920 else if(c_type==ID_unsigned_long_int)
1922 else if(c_type==ID_signed_long_int)
1924 else if(c_type==ID_unsigned_long_long_int)
1926 else if(c_type==ID_signed_long_long_int)
1933 if(sizeof_expr_opt.has_value())
1936 dest =
convert(sizeof_expr_opt.value()) +
" /*" + dest +
"*/ ";
1942 else if(type.
id()==ID_floatbv)
1946 if(!dest.empty() && isdigit(dest[dest.size() - 1]))
1948 if(dest.find(
'.')==std::string::npos)
1958 else if(dest.size()==4 &&
1959 (dest[0]==
'+' || dest[0]==
'-'))
1965 else if(dest ==
"-inf")
1967 else if(dest ==
"+NaN")
1969 else if(dest ==
"-NaN")
1975 std::string suffix =
"";
1986 dest =
"(1.0" + suffix +
"/0.0" + suffix +
")";
1987 else if(dest ==
"-inf")
1988 dest =
"(-1.0" + suffix +
"/0.0" + suffix +
")";
1989 else if(dest ==
"+NaN")
1990 dest =
"(0.0" + suffix +
"/0.0" + suffix +
")";
1991 else if(dest ==
"-NaN")
1992 dest =
"(-0.0" + suffix +
"/0.0" + suffix +
")";
1996 else if(type.
id()==ID_fixedbv)
2000 if(!dest.empty() && isdigit(dest[dest.size() - 1]))
2008 else if(type.
id() == ID_array)
2012 else if(type.
id()==ID_pointer)
2021 dest=
"(("+
convert(type)+
")"+dest+
")";
2024 value ==
"INVALID" || value.
starts_with(
"INVALID-") ||
2025 value ==
"NULL+offset")
2036 else if(type.
id()==ID_string)
2048 unsigned &precedence)
2069 unsigned &precedence)
2072 src, precedence,
configuration.include_struct_padding_components);
2085 unsigned &precedence,
2086 bool include_padding_components)
2088 if(src.
type().
id() != ID_struct && src.
type().
id() != ID_struct_tag)
2092 src.
type().
id() == ID_struct_tag
2099 if(components.size()!=src.
operands().size())
2102 std::string dest=
"{ ";
2104 exprt::operandst::const_iterator o_it=src.
operands().begin();
2113 o_it->type().id() != ID_code,
"struct member must not be of code type");
2115 if(
component.get_is_padding() && !include_padding_components)
2133 std::string tmp=
convert(*o_it);
2135 if(last_size+40<dest.size())
2138 last_size=dest.size();
2158 unsigned &precedence)
2162 if(type.
id() != ID_vector)
2165 std::string dest=
"{ ";
2171 for(
const auto &op : src.
operands())
2185 std::string tmp =
convert(op);
2187 if(last_size+40<dest.size())
2190 last_size=dest.size();
2205 unsigned &precedence)
2207 std::string dest=
"{ ";
2231 bool all_constant=
true;
2233 for(
const auto &op : src.
operands())
2235 if(!op.is_constant())
2240 src.
get_bool(ID_C_string_constant) && all_constant &&
2250 dest.reserve(dest.size()+1+src.
operands().size());
2252 bool last_was_hex=
false;
2273 case '\n': dest+=
"\\n";
break;
2274 case '\t': dest+=
"\\t";
break;
2275 case '\v': dest+=
"\\v";
break;
2276 case '\b': dest+=
"\\b";
break;
2277 case '\r': dest+=
"\\r";
break;
2278 case '\f': dest+=
"\\f";
break;
2279 case '\a': dest+=
"\\a";
break;
2280 case '\\': dest+=
"\\\\";
break;
2281 case '"': dest+=
"\\\"";
break;
2284 if(ch>=
' ' && ch!=127 && ch<0xff)
2285 dest+=
static_cast<char>(ch);
2288 std::ostringstream oss;
2289 oss <<
"\\x" << std::hex << ch;
2307 if(it->is_not_nil())
2327 unsigned &precedence)
2329 std::string dest=
"{ ";
2336 std::string tmp1=
convert(*it);
2340 std::string tmp2=
convert(*it);
2342 std::string tmp=
"["+tmp1+
"]="+tmp2;
2362 if(src.
id()!=ID_compound_literal)
2379 if(src.
id()!=ID_compound_literal)
2418 const auto complement_width_expr =
2423 if(src.
id() == ID_rol)
2426 lhs_expr =
shl_exprt(op0, distance_modulo_width);
2428 rhs_expr =
ashr_exprt(op0, complement_width_expr);
2430 else if(src.
id() == ID_ror)
2433 lhs_expr =
ashr_exprt(op0, distance_modulo_width);
2435 rhs_expr =
shl_exprt(op0, complement_width_expr);
2449 unsigned precedence;
2455 const exprt &designator =
static_cast<const exprt &
>(src.
find(ID_designator));
2456 if(designator.
operands().size() != 1)
2458 unsigned precedence;
2466 if(designator_id.
id() == ID_member)
2468 dest =
"." +
id2string(designator_id.
get(ID_component_name));
2471 designator_id.
id() == ID_index && designator_id.
operands().size() == 1)
2477 unsigned precedence;
2547 unsigned &precedence)
2551 std::string dest=
"overflow(\"";
2561 for(
const auto &op : src.
operands())
2578 return std::string(indent,
' ');
2593 if(!src.
operands()[1].operands().empty() ||
2594 !src.
operands()[2].operands().empty() ||
2595 !src.
operands()[3].operands().empty() ||
2596 !src.
operands()[4].operands().empty())
2604 if(it->operands().size()==2)
2619 if(it->operands().size()==2)
2636 if(it->id()==ID_gcc_asm_clobbered_register)
2665 unsigned precedence;
2691 unsigned precedence;
2720 unsigned precedence;
2757 unsigned precedence;
2799 unsigned precedence;
2815 const exprt &op=*it;
2817 if(op.
get(ID_statement)!=ID_block)
2819 unsigned precedence;
2824 for(
const auto &operand : op.
operands())
2852 unsigned precedence;
2860 const symbolt *symbol=
nullptr;
2871 dest +=
"__declspec(dllexport) ";
2874 if(symbol->
type.
id()==ID_code &&
2896 unsigned precedence;
2909 unsigned precedence;
2947 for(
const auto &statement : src.
statements())
2949 if(statement.get_statement() == ID_label)
2969 for(
const auto &op : src.
operands())
2984 std::string expr_str;
2989 unsigned precedence;
2994 if(dest.empty() || *dest.rbegin()!=
';')
3004 static bool comment_done=
false;
3019 std::ostringstream oss;
3027 [](
const std::pair<irep_idt, irept> &p) { return p.first; });
3038 if(statement==ID_expression)
3041 if(statement==ID_block)
3044 if(statement==ID_switch)
3047 if(statement==ID_for)
3050 if(statement==ID_while)
3053 if(statement==ID_asm)
3056 if(statement==ID_skip)
3059 if(statement==ID_dowhile)
3062 if(statement==ID_ifthenelse)
3065 if(statement==ID_return)
3068 if(statement==ID_goto)
3071 if(statement==ID_printf)
3074 if(statement==ID_fence)
3083 if(statement==ID_assume)
3086 if(statement==ID_assert)
3089 if(statement==ID_break)
3092 if(statement==ID_continue)
3095 if(statement==ID_decl)
3098 if(statement==ID_decl_block)
3101 if(statement==ID_dead)
3104 if(statement==ID_assign)
3107 if(statement==
"lock")
3110 if(statement==
"unlock")
3113 if(statement==ID_atomic_begin)
3116 if(statement==ID_atomic_end)
3119 if(statement==ID_function_call)
3122 if(statement==ID_label)
3125 if(statement==ID_switch_case)
3128 if(statement==ID_array_set)
3131 if(statement==ID_array_copy)
3134 if(statement==ID_array_replace)
3137 if(statement == ID_set_may || statement == ID_set_must)
3141 unsigned precedence;
3159 unsigned precedence;
3172 unsigned precedence;
3185 unsigned precedence;
3216 if(it!=arguments.begin())
3231 std::string dest=
indent_str(indent)+
"printf(";
3253 std::string dest=
indent_str(indent)+
"FENCE(";
3256 { ID_WRfence, ID_RRfence, ID_RWfence, ID_WWfence,
3257 ID_RRcumul, ID_RWcumul, ID_WWcumul, ID_WRcumul,
3262 for(
unsigned i=0; !att[i].
empty(); i++)
3283 std::string dest=
indent_str(indent)+
"INPUT(";
3305 std::string dest=
indent_str(indent)+
"OUTPUT(";
3326 std::string dest=
indent_str(indent)+
"ARRAY_SET(";
3348 std::string dest=
indent_str(indent)+
"ARRAY_COPY(";
3370 std::string dest=
indent_str(indent)+
"ARRAY_REPLACE(";
3393 unsigned precedence;
3406 unsigned precedence;
3418 std::string labels_string;
3422 labels_string+=
"\n";
3425 labels_string+=
":\n";
3429 return labels_string+tmp;
3436 std::string labels_string;
3440 labels_string+=
"\n";
3442 labels_string+=
"default:\n";
3446 labels_string+=
"\n";
3448 labels_string+=
"case ";
3450 labels_string+=
":\n";
3453 unsigned next_indent=indent;
3459 return labels_string+tmp;
3469 unsigned precedence;
3477 static_cast<const codet &
>(src.
find(ID_code));
3479 std::string dest=
"\n";
3484 std::string assumption_str=
convert(assumption);
3486 dest+=assumption_str;
3499 std::string assertion_str=
convert(assertion);
3501 dest+=assertion_str;
3527 if(expr_width_opt.has_value())
3545 unsigned &precedence)
3550 std::string dest=
"sizeof(";
3561 const auto &cond = src.
operands().front();
3568 const auto &targets = src.
operands()[1];
3573 if(it != targets.operands().begin())
3586 const std::size_t width = type_ptr->get_width();
3587 if(width == 8 || width == 16 || width == 32 || width == 64)
3590 src,
"__builtin_bitreverse" + std::to_string(width));
3594 unsigned precedence;
3600 std::string dest = src.
id() == ID_r_ok ?
"R_OK"
3601 : src.
id() == ID_w_ok ?
"W_OK"
3620 std::string dest = src.
id() == ID_prophecy_r_ok ?
"R_OK"
3621 : src.
id() == ID_prophecy_w_ok ?
"W_OK"
3676 unsigned &precedence)
3680 if(src.
id()==ID_plus)
3683 else if(src.
id()==ID_minus)
3686 else if(src.
id()==ID_unary_minus)
3689 else if(src.
id()==ID_unary_plus)
3692 else if(src.
id()==ID_floatbv_typecast)
3696 std::string dest=
"FLOAT_TYPECAST(";
3725 else if(src.
id()==ID_sign)
3733 else if(src.
id()==ID_popcount)
3741 else if(src.
id()==
"pointer_arithmetic")
3744 else if(src.
id()==
"pointer_difference")
3747 else if(src.
id() == ID_null_object)
3748 return "NULL-object";
3750 else if(src.
id()==ID_integer_address ||
3751 src.
id()==ID_integer_address_object ||
3752 src.
id()==ID_stack_object ||
3753 src.
id()==ID_static_object)
3758 else if(src.
id()==
"builtin-function")
3761 else if(src.
id()==ID_array_of)
3764 else if(src.
id()==ID_bswap)
3776 else if(src.
id()==ID_address_of)
3780 if(
object.
id() == ID_label)
3781 return "&&" +
object.
get_string(ID_identifier);
3782 else if(
object.
id() == ID_index &&
to_index_expr(
object).index().is_zero())
3790 else if(src.
id()==ID_dereference)
3794 if(src.
type().
id() == ID_code)
3797 pointer.id() == ID_plus && pointer.operands().size() == 2 &&
3807 else if(src.
id()==ID_index)
3810 else if(src.
id()==ID_member)
3813 else if(src.
id()==
"array-member-value")
3816 else if(src.
id()==
"struct-member-value")
3819 else if(src.
id()==ID_function_application)
3822 else if(src.
id()==ID_side_effect)
3825 if(statement==ID_preincrement)
3827 else if(statement==ID_predecrement)
3829 else if(statement==ID_postincrement)
3831 else if(statement==ID_postdecrement)
3833 else if(statement==ID_assign_plus)
3835 else if(statement==ID_assign_minus)
3837 else if(statement==ID_assign_mult)
3839 else if(statement==ID_assign_div)
3841 else if(statement==ID_assign_mod)
3843 else if(statement==ID_assign_shl)
3845 else if(statement==ID_assign_shr)
3847 else if(statement==ID_assign_bitand)
3849 else if(statement==ID_assign_bitxor)
3851 else if(statement==ID_assign_bitor)
3853 else if(statement==ID_assign)
3855 else if(statement==ID_function_call)
3858 else if(statement == ID_allocate)
3860 else if(statement==ID_printf)
3862 else if(statement==ID_nondet)
3864 else if(statement==
"prob_coin")
3866 else if(statement==
"prob_unif")
3868 else if(statement==ID_statement_expression)
3870 else if(statement == ID_va_start)
3876 else if(src.
id()==ID_literal)
3879 else if(src.
id()==ID_not)
3882 else if(src.
id()==ID_bitnot)
3885 else if(src.
id()==ID_mult)
3888 else if(src.
id()==ID_div)
3891 else if(src.
id()==ID_mod)
3894 else if(src.
id()==ID_shl)
3897 else if(src.
id()==ID_ashr || src.
id()==ID_lshr)
3900 else if(src.
id()==ID_lt || src.
id()==ID_gt ||
3901 src.
id()==ID_le || src.
id()==ID_ge)
3907 else if(src.
id()==ID_notequal)
3910 else if(src.
id()==ID_equal)
3913 else if(src.
id()==ID_complex)
3916 else if(src.
id()==ID_bitand)
3919 else if(src.
id()==ID_bitxor)
3922 else if(src.
id()==ID_bitor)
3925 else if(src.
id()==ID_and)
3928 else if(src.
id()==ID_or)
3931 else if(src.
id()==ID_xor)
3934 else if(src.
id()==ID_implies)
3937 else if(src.
id()==ID_if)
3940 else if(src.
id()==ID_forall)
3943 else if(src.
id()==ID_exists)
3946 else if(src.
id()==ID_lambda)
3949 else if(src.
id()==ID_with)
3952 else if(src.
id()==ID_update)
3955 else if(src.
id()==ID_member_designator)
3958 else if(src.
id()==ID_index_designator)
3961 else if(src.
id()==ID_symbol)
3964 else if(src.
id()==ID_nondet_symbol)
3967 else if(src.
id()==ID_predicate_symbol)
3970 else if(src.
id()==ID_predicate_next_symbol)
3973 else if(src.
id()==ID_predicate_passive_symbol)
3976 else if(src.
id()==
"quant_symbol")
3979 else if(src.
id()==ID_nondet_bool)
3982 else if(src.
id()==ID_object_descriptor)
3985 else if(src.
id()==
"Hoare")
3988 else if(src.
id()==ID_code)
3994 else if(src.
id() == ID_annotated_pointer_constant)
4000 else if(src.
id()==ID_string_constant)
4003 else if(src.
id()==ID_struct)
4006 else if(src.
id()==ID_vector)
4009 else if(src.
id()==ID_union)
4012 else if(src.
id()==ID_array)
4015 else if(src.
id() == ID_array_list)
4018 else if(src.
id()==ID_typecast)
4021 else if(src.
id()==ID_comma)
4024 else if(src.
id()==ID_ptr_object)
4025 return "PTR_OBJECT("+
id2string(src.
get(ID_identifier))+
")";
4027 else if(src.
id()==ID_cond)
4037 else if(src.
id()==ID_unknown)
4040 else if(src.
id()==ID_invalid)
4043 else if(src.
id()==ID_extractbit)
4046 else if(src.
id()==ID_extractbits)
4049 else if(src.
id()==ID_initializer_list ||
4050 src.
id()==ID_compound_literal)
4056 else if(src.
id()==ID_designated_initializer)
4062 else if(src.
id()==ID_sizeof)
4065 else if(src.
id()==ID_let)
4068 else if(src.
id()==ID_type)
4071 else if(src.
id() == ID_rol || src.
id() == ID_ror)
4074 else if(src.
id() == ID_conditional_target_group)
4079 else if(src.
id() == ID_bitreverse)
4082 else if(src.
id() == ID_r_ok || src.
id() == ID_w_ok || src.
id() == ID_rw_ok)
4086 auto prophecy_r_or_w_ok =
4092 else if(src.
id() == ID_pointer_in_range)
4095 else if(src.
id() == ID_prophecy_pointer_in_range)
4102 if(function_string_opt.has_value())
4103 return *function_string_opt;
4111 static const std::map<irep_idt, std::string> function_names = {
4112 {
"buffer_size",
"BUFFER_SIZE"},
4113 {
"is_zero_string",
"IS_ZERO_STRING"},
4114 {
"object_value",
"OBJECT_VALUE"},
4115 {
"pointer_base",
"POINTER_BASE"},
4116 {
"pointer_cons",
"POINTER_CONS"},
4117 {
"zero_string",
"ZERO_STRING"},
4118 {
"zero_string_length",
"ZERO_STRING_LENGTH"},
4120 {ID_alignof,
"alignof"},
4121 {ID_builtin_offsetof,
"builtin_offsetof"},
4122 {ID_complex_imag,
"__imag__"},
4123 {ID_complex_real,
"__real__"},
4124 {ID_concatenation,
"CONCATENATION"},
4125 {ID_count_leading_zeros,
"__builtin_clz"},
4126 {ID_count_trailing_zeros,
"__builtin_ctz"},
4127 {ID_dynamic_object,
"DYNAMIC_OBJECT"},
4128 {ID_live_object,
"LIVE_OBJECT"},
4129 {ID_writeable_object,
"WRITEABLE_OBJECT"},
4130 {ID_find_first_set,
"__builtin_ffs"},
4131 {ID_separate,
"SEPARATE"},
4132 {ID_floatbv_div,
"FLOAT/"},
4133 {ID_floatbv_minus,
"FLOAT-"},
4134 {ID_floatbv_mult,
"FLOAT*"},
4135 {ID_floatbv_plus,
"FLOAT+"},
4136 {ID_floatbv_rem,
"FLOAT%"},
4137 {ID_gcc_builtin_va_arg,
"gcc_builtin_va_arg"},
4140 {ID_ieee_float_equal,
"IEEE_FLOAT_EQUAL"},
4141 {ID_ieee_float_notequal,
"IEEE_FLOAT_NOTEQUAL"},
4142 {ID_infinity,
"INFINITY"},
4143 {ID_is_dynamic_object,
"IS_DYNAMIC_OBJECT"},
4144 {ID_is_invalid_pointer,
"IS_INVALID_POINTER"},
4146 {ID_isfinite,
"isfinite"},
4147 {ID_isinf,
"isinf"},
4148 {ID_isnan,
"isnan"},
4149 {ID_isnormal,
"isnormal"},
4156 {ID_width,
"WIDTH"},
4159 const auto function_entry = function_names.find(src.
id());
4160 if(function_entry == function_names.end())
4168 unsigned precedence;
4179 const std::string &identifier)
4191 expr2c.get_shorthands(expr);
4192 return expr2c.convert(expr);
4207 return expr2c.convert(type);
4217 const std::string &identifier,
4222 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 bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
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.
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
exprt & symbolic_pointer()
const typet & element_type() const
The type of the elements of the array.
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...
const typet & underlying_type() const
C enum tag type, i.e., c_enum_typet with an identifier.
const typet & underlying_type() const
std::vector< c_enum_membert > memberst
virtual void read(const typet &src)
virtual std::unique_ptr< c_qualifierst > clone() const
virtual std::string as_string() const
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
const parameterst & parameters() const
const typet & return_type() const
bool has_ellipsis() const
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
A constant literal expression.
const irep_idt & get_value() const
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
const char * c_str() const
std::optional< 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_nondet(const exprt &src, unsigned &precedence)
std::string convert_literal(const exprt &src)
std::string convert_code_continue(unsigned indent)
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)
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
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)
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)
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)
virtual std::string convert_array_type(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator_str)
To generate a C-like type declaration of an array.
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::size_t get_fraction_bits() 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
signed int get_int(const irep_idt &name) 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()
std::string expr2string() const
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
const typet & base_type() const
The type of the data what we point to.
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
const irept::named_subt & get_pragmas() const
const irep_idt & get_comment() const
A struct tag type, i.e., struct_typet with an identifier.
Structure type, corresponds to C style structs.
const irep_idt & get_pretty_name() const
Base type for structs and unions.
const componentst & components() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
bool is_incomplete() const
A struct/union may be incomplete.
std::vector< componentt > componentst
Expression to hold a symbol (variable)
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
An expression with three operands.
const typet & subtype() const
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.
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
bool has_prefix(const std::string &s, const std::string &prefix)
static std::unordered_set< irep_idt > find_symbol_identifiers(const goto_programt &src)
Find all identifiers in src.
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
static std::optional< 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 can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto type_checked_cast(TType &base) -> typename detail::expr_dynamic_cast_return_typet< T, TType >::type
Cast a reference to a generic typet to a specific derived class and checks that the type could be con...
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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)
static std::string binary(const constant_exprt &src)
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 mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
const std::string integer2string(const mp_integer &n, unsigned base)
const std::string integer2binary(const mp_integer &n, std::size_t width)
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.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(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 struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_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?