Go to the documentation of this file.
89 if(
pos!=std::string::npos)
100 if(c_pos!=std::string::npos &&
101 dest.rfind(
"::")==c_pos)
102 dest.erase(0, c_pos+2);
103 else if(c_pos!=std::string::npos)
123 for(
const auto &symbol_id : symbols)
134 func = func.substr(0, func.rfind(
"::"));
144 if(!
shorthands.insert(std::make_pair(symbol_id, sh)).second)
148 for(
const auto &symbol_id : symbols)
164 has_collision=!
ns.
lookup(sh, symbol);
183 shorthands.insert(std::make_pair(symbol_id, sh));
195 const std::string &declarator)
197 std::unique_ptr<qualifierst> clone = qualifiers.
clone();
199 new_qualifiers.
read(src);
201 std::string q=new_qualifiers.
as_string();
203 std::string d = declarator.empty() ? declarator :
" " + declarator;
210 if(src.
id()==ID_bool)
214 else if(src.
id()==ID_c_bool)
218 else if(src.
id()==ID_string)
222 else if(src.
id()==ID_natural ||
223 src.
id()==ID_integer ||
224 src.
id()==ID_rational)
228 else if(src.
id()==ID_empty)
232 else if(src.
id()==ID_complex)
237 else if(src.
id()==ID_floatbv)
246 return q+
"long double"+d;
251 return q +
CPROVER_PREFIX +
"floatbv[" + swidth +
"][" + fwidth +
"]";
254 else if(src.
id()==ID_fixedbv)
262 else if(src.
id()==ID_c_bit_field)
267 else if(src.
id()==ID_signedbv ||
268 src.
id()==ID_unsignedbv)
274 if(c_type==ID_char &&
277 if(src.
id()==ID_signedbv)
278 return q+
"signed char"+d;
280 return q+
"unsigned char"+d;
282 else if(c_type!=ID_wchar_t && !c_type_str.
empty())
283 return q+c_type_str+d;
290 std::string sign_str=
is_signed?
"signed ":
"unsigned ";
296 return q+sign_str+
"int"+d;
302 return q+sign_str+
"long int"+d;
307 return q+sign_str+
"char"+d;
313 return q+sign_str+
"short int"+d;
319 return q+sign_str+
"long long int"+d;
325 return q + sign_str +
"__int128" + d;
333 else if(src.
id()==ID_struct)
337 else if(src.
id()==ID_union)
341 std::string dest=q+
"union";
365 else if(src.
id()==ID_c_enum)
396 for(c_enum_typet::memberst::const_iterator it = members.begin();
402 if(it != members.begin())
405 result +=
id2string(it->get_base_name());
416 else if(src.
id()==ID_c_enum_tag)
420 std::string result=q+
"enum";
425 else if(src.
id()==ID_pointer)
432 std::string new_declarator=
"*";
434 if(!q.empty() && (!declarator.empty() || subtype.
id() == ID_pointer))
436 new_declarator+=
" "+q;
439 new_declarator+=declarator;
443 subtype.
id() == ID_code ||
446 new_declarator=
"("+new_declarator+
")";
449 return convert_rec(subtype, sub_qualifiers, new_declarator);
451 else if(src.
id()==ID_array)
455 else if(src.
id()==ID_struct_tag)
460 std::string dest=q+
"struct";
468 else if(src.
id()==ID_union_tag)
473 std::string dest=q+
"union";
481 else if(src.
id()==ID_code)
487 std::string dest=declarator+
"(";
491 if(parameters.empty())
498 for(code_typet::parameterst::const_iterator
499 it=parameters.begin();
500 it!=parameters.end();
503 if(it!=parameters.begin())
506 if(it->get_identifier().empty())
510 std::string arg_declarator=
535 const typet *non_ptr_type = &return_type;
536 while(non_ptr_type->
id()==ID_pointer)
537 non_ptr_type = &(non_ptr_type->
subtype());
539 if(non_ptr_type->
id()==ID_code ||
540 non_ptr_type->
id()==ID_array)
541 dest=
convert_rec(return_type, ret_qualifiers, dest);
543 dest=
convert_rec(return_type, ret_qualifiers,
"")+
" "+dest;
549 if(dest[dest.size()-1]==
' ')
550 dest.resize(dest.size()-1);
555 else if(src.
id()==ID_vector)
559 const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.
size());
564 if(tmp==
"signed char" || tmp==
"char")
566 else if(tmp==
"signed short int")
568 else if(tmp==
"signed int")
570 else if(tmp==
"signed long long int")
572 else if(tmp==
"float")
574 else if(tmp==
"double")
580 dest+=
" __attribute__((vector_size (";
582 dest+=
"*sizeof("+subtype+
"))))";
587 else if(src.
id()==ID_constructor ||
588 src.
id()==ID_destructor)
590 return q+
"__attribute__(("+
id2string(src.
id())+
")) void"+d;
611 const std::string &qualifiers_str,
612 const std::string &declarator_str)
634 const std::string &qualifiers,
635 const std::string &declarator,
636 bool inc_struct_body,
637 bool inc_padding_components)
642 assert(inc_struct_body || !inc_padding_components);
646 std::string dest=qualifiers+
"struct";
659 if(
component.get_is_padding() && !inc_padding_components)
689 const std::string &declarator_str)
706 const std::string &declarator_str,
707 bool inc_size_if_possible)
710 std::string array_suffix;
712 if(
to_array_type(src).size().is_nil() || !inc_size_if_possible)
720 src.
subtype(), qualifiers, declarator_str+array_suffix);
725 unsigned &precedence)
735 if(to_type.
id()==ID_c_bool &&
739 if(to_type.
id()==ID_bool &&
743 std::string dest =
"(" +
convert(to_type) +
")";
759 const std::string &symbol1,
760 const std::string &symbol2,
806 const std::string &symbol,
818 std::string dest=symbol+
" { ";
848 for(
size_t i=1; i<src.
operands().size(); i+=2)
850 std::string op1, op2;
856 if(src.
operands()[i].id()==ID_member_name)
859 src.
operands()[i].get(ID_component_name);
874 display_component_name=component_name;
878 op1=
"."+
id2string(display_component_name);
906 std::string dest=
"LET ";
923 std::string op0, op1, op2;
937 const exprt &designator = src.
op1();
964 std::string dest=
"cond {\n";
981 condition=!condition;
991 const std::string &symbol,
993 bool full_parentheses)
1012 bool use_parentheses0=
1014 (precedence==p0 && full_parentheses) ||
1015 (precedence==p0 && src.
id()!=op0.
id());
1017 if(use_parentheses0)
1020 if(use_parentheses0)
1027 bool use_parentheses1=
1029 (precedence==p1 && full_parentheses) ||
1030 (precedence==p1 && src.
id()!=op1.
id());
1032 if(use_parentheses1)
1035 if(use_parentheses1)
1043 const std::string &symbol,
1044 unsigned precedence,
1045 bool full_parentheses)
1075 bool use_parentheses=
1077 (precedence==p && full_parentheses) ||
1078 (precedence==p && src.
id()!=it->id());
1092 const std::string &symbol,
1093 unsigned precedence)
1098 std::string dest=symbol;
1121 std::string dest =
"ALLOCATE";
1124 if(src.
type().
id()==ID_pointer &&
1131 dest += op0 +
", " + op1;
1139 unsigned &precedence)
1149 unsigned &precedence)
1164 unsigned &precedence)
1179 unsigned &precedence)
1182 return "PROB_UNIFORM(" +
convert(src.
type()) +
"," +
1190 std::string dest=name;
1211 unsigned precedence)
1218 if(*op0.rbegin()==
';')
1219 op0.resize(op0.size()-1);
1223 if(*op1.rbegin()==
';')
1224 op1.resize(op1.size()-1);
1226 std::string dest=op0;
1235 unsigned precedence)
1264 std::string dest=name;
1285 unsigned precedence)
1295 unsigned precedence)
1346 const std::string &symbol,
1347 unsigned precedence)
1368 unsigned precedence)
1391 const exprt &src,
unsigned &precedence)
1396 std::string dest=
"POINTER_ARITHMETIC(";
1428 const exprt &src,
unsigned &precedence)
1435 std::string dest=
"POINTER_DIFFERENCE(";
1440 op =
convert(binary_expr.op0().type());
1468 unsigned precedence;
1473 return "."+src.
get_string(ID_component_name);
1478 unsigned precedence;
1488 unsigned precedence)
1490 const auto &compound = src.
compound();
1495 if(compound.id() == ID_dereference)
1501 if(precedence > p || pointer.id() == ID_typecast)
1504 if(precedence > p || pointer.id() == ID_typecast)
1513 if(precedence > p || compound.id() == ID_typecast)
1516 if(precedence > p || compound.id() == ID_typecast)
1524 if(full_type.
id()!=ID_struct &&
1525 full_type.
id()!=ID_union)
1533 if(!component_name.
empty())
1540 if(!comp_expr.
get(ID_pretty_name).
empty())
1562 unsigned precedence)
1572 unsigned precedence)
1582 unsigned &precedence)
1598 to_unary_expr(src).op().
id() == ID_predicate_passive_symbol)
1604 std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
1628 if(src.
id()==ID_next_symbol)
1629 dest=
"NEXT("+dest+
")";
1637 return "nondet_symbol("+
id2string(
id)+
")";
1642 const std::string &
id=src.
get_string(ID_identifier);
1643 return "ps("+
id+
")";
1648 const std::string &
id=src.
get_string(ID_identifier);
1649 return "pns("+
id+
")";
1654 const std::string &
id=src.
get_string(ID_identifier);
1655 return "pps("+
id+
")";
1660 const std::string &
id=src.
get_string(ID_identifier);
1666 return "nondet_bool()";
1671 unsigned &precedence)
1676 std::string result=
"<";
1695 unsigned &precedence)
1702 if(type.
id()==ID_integer ||
1703 type.
id()==ID_natural ||
1704 type.
id()==ID_rational)
1708 else if(type.
id()==ID_c_enum ||
1709 type.
id()==ID_c_enum_tag)
1715 if(c_enum_type.
id()!=ID_c_enum)
1723 for(
const auto &member : members)
1725 if(member.get_value() == value)
1726 return "/*enum*/" +
id2string(member.get_base_name());
1734 std::string value_as_string =
1738 return value_as_string;
1740 return "/*enum*/" + value_as_string;
1742 else if(type.
id()==ID_rational)
1744 else if(type.
id()==ID_bv)
1749 else if(type.
id()==ID_bool)
1753 else if(type.
id()==ID_unsignedbv ||
1754 type.
id()==ID_signedbv ||
1755 type.
id()==ID_c_bit_field ||
1756 type.
id()==ID_c_bool)
1764 type.
id()==ID_c_bit_field?type.
subtype().
get(ID_C_c_type):
1765 type.
get(ID_C_c_type);
1767 if(type.
id()==ID_c_bool)
1777 else if(int_value==
'\r')
1779 else if(int_value==
'\t')
1781 else if(int_value==
'\'')
1783 else if(int_value==
'\\')
1785 else if(int_value>=
' ' && int_value<126)
1788 dest += numeric_cast_v<char>(int_value);
1805 if(c_type==ID_unsigned_int)
1807 else if(c_type==ID_unsigned_long_int)
1809 else if(c_type==ID_signed_long_int)
1811 else if(c_type==ID_unsigned_long_long_int)
1813 else if(c_type==ID_signed_long_long_int)
1819 const auto sizeof_expr_opt =
1822 if(sizeof_expr_opt.has_value())
1825 dest =
convert(sizeof_expr_opt.value()) +
" /*" + dest +
"*/ ";
1831 else if(type.
id()==ID_floatbv)
1835 if(!dest.empty() && isdigit(dest[dest.size() - 1]))
1837 if(dest.find(
'.')==std::string::npos)
1847 else if(dest.size()==4 &&
1848 (dest[0]==
'+' || dest[0]==
'-'))
1854 else if(dest ==
"-inf")
1856 else if(dest ==
"+NaN")
1858 else if(dest ==
"-NaN")
1864 std::string suffix =
"";
1875 dest =
"(1.0" + suffix +
"/0.0" + suffix +
")";
1876 else if(dest ==
"-inf")
1877 dest =
"(-1.0" + suffix +
"/0.0" + suffix +
")";
1878 else if(dest ==
"+NaN")
1879 dest =
"(0.0" + suffix +
"/0.0" + suffix +
")";
1880 else if(dest ==
"-NaN")
1881 dest =
"(-0.0" + suffix +
"/0.0" + suffix +
")";
1885 else if(type.
id()==ID_fixedbv)
1889 if(!dest.empty() && isdigit(dest[dest.size() - 1]))
1897 else if(type.
id() == ID_array)
1901 else if(type.
id()==ID_pointer)
1912 dest=
"(("+
convert(type)+
")"+dest+
")";
1914 else if(src.
operands().size() == 1)
1918 if(annotation.id() == ID_constant)
1922 if(op_value==
"INVALID" ||
1924 op_value==
"NULL+offset")
1939 else if(type.
id()==ID_string)
1963 unsigned &precedence)
1979 unsigned &precedence,
1980 bool include_padding_components)
1984 if(full_type.
id()!=ID_struct)
1993 if(components.size()!=src.
operands().size())
1996 std::string dest=
"{ ";
1998 exprt::operandst::const_iterator o_it=src.
operands().begin();
2006 if(o_it->type().id()==ID_code)
2009 if(
component.get_is_padding() && !include_padding_components)
2027 std::string tmp=
convert(*o_it);
2029 if(last_size+40<dest.size())
2032 last_size=dest.size();
2052 unsigned &precedence)
2056 if(type.
id() != ID_vector)
2059 std::string dest=
"{ ";
2081 if(last_size+40<dest.size())
2084 last_size=dest.size();
2099 unsigned &precedence)
2101 std::string dest=
"{ ";
2125 bool all_constant=
true;
2128 if(!it->is_constant())
2131 if(src.
get_bool(ID_C_string_constant) &&
2142 dest.reserve(dest.size()+1+src.
operands().size());
2144 bool last_was_hex=
false;
2165 case '\n': dest+=
"\\n";
break;
2166 case '\t': dest+=
"\\t";
break;
2167 case '\v': dest+=
"\\v";
break;
2168 case '\b': dest+=
"\\b";
break;
2169 case '\r': dest+=
"\\r";
break;
2170 case '\f': dest+=
"\\f";
break;
2171 case '\a': dest+=
"\\a";
break;
2172 case '\\': dest+=
"\\\\";
break;
2173 case '"': dest+=
"\\\"";
break;
2176 if(ch>=
' ' && ch!=127 && ch<0xff)
2177 dest+=
static_cast<char>(ch);
2180 std::ostringstream oss;
2181 oss <<
"\\x" << std::hex << ch;
2199 if(it->is_not_nil())
2219 unsigned &precedence)
2221 std::string dest=
"{ ";
2228 std::string tmp1=
convert(*it);
2232 std::string tmp2=
convert(*it);
2234 std::string tmp=
"["+tmp1+
"]="+tmp2;
2254 if(src.
id()!=ID_compound_literal)
2271 if(src.
id()!=ID_compound_literal)
2281 unsigned precedence;
2287 const exprt &designator =
static_cast<const exprt &
>(src.
find(ID_designator));
2288 if(designator.
operands().size() != 1)
2290 unsigned precedence;
2298 if(designator_id.
id() == ID_member)
2300 dest =
"." +
id2string(designator_id.
get(ID_component_name));
2303 designator_id.
id() == ID_index && designator_id.
operands().size() == 1)
2309 unsigned precedence;
2379 unsigned &precedence)
2383 std::string dest=
"overflow(\"";
2410 return std::string(indent,
' ');
2425 if(!src.
operands()[1].operands().empty() ||
2426 !src.
operands()[2].operands().empty() ||
2427 !src.
operands()[3].operands().empty() ||
2428 !src.
operands()[4].operands().empty())
2436 if(it->operands().size()==2)
2451 if(it->operands().size()==2)
2468 if(it->id()==ID_gcc_asm_clobbered_register)
2497 unsigned precedence;
2523 unsigned precedence;
2552 unsigned precedence;
2589 unsigned precedence;
2631 unsigned precedence;
2647 const exprt &op=*it;
2649 if(op.
get(ID_statement)!=ID_block)
2651 unsigned precedence;
2685 unsigned precedence;
2693 const symbolt *symbol=
nullptr;
2704 dest +=
"__declspec(dllexport) ";
2707 if(symbol->
type.
id()==ID_code &&
2729 unsigned precedence;
2742 unsigned precedence;
2780 for(
const auto &statement : src.
statements())
2782 if(statement.get_statement() == ID_label)
2817 std::string expr_str;
2822 unsigned precedence;
2827 if(dest.empty() || *dest.rbegin()!=
';')
2837 static bool comment_done=
false;
2852 std::ostringstream oss;
2860 [](
const std::pair<irep_idt, irept> &p) { return p.first; });
2871 if(statement==ID_expression)
2874 if(statement==ID_block)
2877 if(statement==ID_switch)
2880 if(statement==ID_for)
2883 if(statement==ID_while)
2886 if(statement==ID_asm)
2889 if(statement==ID_skip)
2892 if(statement==ID_dowhile)
2895 if(statement==ID_ifthenelse)
2898 if(statement==ID_return)
2901 if(statement==ID_goto)
2904 if(statement==ID_printf)
2907 if(statement==ID_fence)
2916 if(statement==ID_assume)
2919 if(statement==ID_assert)
2922 if(statement==ID_break)
2925 if(statement==ID_continue)
2928 if(statement==ID_decl)
2931 if(statement==ID_decl_block)
2934 if(statement==ID_dead)
2937 if(statement==ID_assign)
2940 if(statement==
"lock")
2943 if(statement==
"unlock")
2946 if(statement==ID_atomic_begin)
2949 if(statement==ID_atomic_end)
2952 if(statement==ID_function_call)
2955 if(statement==ID_label)
2958 if(statement==ID_switch_case)
2961 if(statement==ID_array_set)
2964 if(statement==ID_array_copy)
2967 if(statement==ID_array_replace)
2970 if(statement == ID_set_may || statement == ID_set_must)
2974 unsigned precedence;
2992 unsigned precedence;
3005 unsigned precedence;
3018 unsigned precedence;
3049 if(it!=arguments.begin())
3064 std::string dest=
indent_str(indent)+
"printf(";
3086 std::string dest=
indent_str(indent)+
"FENCE(";
3089 { ID_WRfence, ID_RRfence, ID_RWfence, ID_WWfence,
3090 ID_RRcumul, ID_RWcumul, ID_WWcumul, ID_WRcumul,
3095 for(
unsigned i=0; !att[i].
empty(); i++)
3116 std::string dest=
indent_str(indent)+
"INPUT(";
3138 std::string dest=
indent_str(indent)+
"OUTPUT(";
3159 std::string dest=
indent_str(indent)+
"ARRAY_SET(";
3181 std::string dest=
indent_str(indent)+
"ARRAY_COPY(";
3203 std::string dest=
indent_str(indent)+
"ARRAY_REPLACE(";
3226 unsigned precedence;
3239 unsigned precedence;
3251 std::string labels_string;
3255 labels_string+=
"\n";
3258 labels_string+=
":\n";
3262 return labels_string+tmp;
3269 std::string labels_string;
3273 labels_string+=
"\n";
3275 labels_string+=
"default:\n";
3279 labels_string+=
"\n";
3281 labels_string+=
"case ";
3283 labels_string+=
":\n";
3286 unsigned next_indent=indent;
3292 return labels_string+tmp;
3302 unsigned precedence;
3310 static_cast<const codet &
>(src.
find(ID_code));
3312 std::string dest=
"\n";
3317 std::string assumption_str=
convert(assumption);
3319 dest+=assumption_str;
3332 std::string assertion_str=
convert(assertion);
3334 dest+=assertion_str;
3369 unsigned &precedence)
3374 std::string dest=
"sizeof(";
3383 unsigned &precedence)
3387 if(src.
id()==ID_plus)
3390 else if(src.
id()==ID_minus)
3393 else if(src.
id()==ID_unary_minus)
3396 else if(src.
id()==ID_unary_plus)
3399 else if(src.
id()==ID_floatbv_plus)
3402 else if(src.
id()==ID_floatbv_minus)
3405 else if(src.
id()==ID_floatbv_mult)
3408 else if(src.
id()==ID_floatbv_div)
3411 else if(src.
id()==ID_floatbv_rem)
3414 else if(src.
id()==ID_floatbv_typecast)
3418 std::string dest=
"FLOAT_TYPECAST(";
3447 else if(src.
id()==ID_sign)
3455 else if(src.
id()==ID_popcount)
3463 else if(src.
id() == ID_r_ok)
3466 else if(src.
id() == ID_w_ok)
3469 else if(src.
id() == ID_is_invalid_pointer)
3472 else if(src.
id()==ID_good_pointer)
3475 else if(src.
id()==ID_object_size)
3478 else if(src.
id()==
"pointer_arithmetic")
3481 else if(src.
id()==
"pointer_difference")
3484 else if(src.
id() == ID_null_object)
3485 return "NULL-object";
3487 else if(src.
id()==ID_integer_address ||
3488 src.
id()==ID_integer_address_object ||
3489 src.
id()==ID_stack_object ||
3490 src.
id()==ID_static_object)
3495 else if(src.
id()==ID_infinity)
3498 else if(src.
id()==
"builtin-function")
3501 else if(src.
id()==ID_pointer_object)
3504 else if(src.
id() == ID_get_must)
3507 else if(src.
id() == ID_get_may)
3510 else if(src.
id()==
"object_value")
3513 else if(src.
id()==ID_array_of)
3516 else if(src.
id()==ID_pointer_offset)
3519 else if(src.
id()==
"pointer_base")
3522 else if(src.
id()==
"pointer_cons")
3525 else if(src.
id() == ID_is_invalid_pointer)
3528 else if(src.
id() == ID_dynamic_object)
3531 else if(src.
id() == ID_is_dynamic_object)
3534 else if(src.
id()==
"is_zero_string")
3537 else if(src.
id()==
"zero_string")
3540 else if(src.
id()==
"zero_string_length")
3543 else if(src.
id()==
"buffer_size")
3546 else if(src.
id()==ID_isnan)
3549 else if(src.
id()==ID_isfinite)
3552 else if(src.
id()==ID_isinf)
3555 else if(src.
id()==ID_bswap)
3561 else if(src.
id()==ID_isnormal)
3564 else if(src.
id()==ID_builtin_offsetof)
3567 else if(src.
id()==ID_gcc_builtin_va_arg)
3570 else if(src.
id()==ID_alignof)
3580 else if(src.
id()==ID_address_of)
3584 if(
object.
id() == ID_label)
3585 return "&&" +
object.
get_string(ID_identifier);
3586 else if(
object.
id() == ID_index &&
to_index_expr(
object).index().is_zero())
3594 else if(src.
id()==ID_dereference)
3598 if(src.
type().
id() == ID_code)
3601 pointer.id() == ID_plus && pointer.operands().size() == 2 &&
3612 else if(src.
id()==ID_index)
3615 else if(src.
id()==ID_member)
3618 else if(src.
id()==
"array-member-value")
3621 else if(src.
id()==
"struct-member-value")
3624 else if(src.
id()==ID_function_application)
3627 else if(src.
id()==ID_side_effect)
3630 if(statement==ID_preincrement)
3632 else if(statement==ID_predecrement)
3634 else if(statement==ID_postincrement)
3636 else if(statement==ID_postdecrement)
3638 else if(statement==ID_assign_plus)
3640 else if(statement==ID_assign_minus)
3642 else if(statement==ID_assign_mult)
3644 else if(statement==ID_assign_div)
3646 else if(statement==ID_assign_mod)
3648 else if(statement==ID_assign_shl)
3650 else if(statement==ID_assign_shr)
3652 else if(statement==ID_assign_bitand)
3654 else if(statement==ID_assign_bitxor)
3656 else if(statement==ID_assign_bitor)
3658 else if(statement==ID_assign)
3660 else if(statement==ID_function_call)
3663 else if(statement == ID_allocate)
3665 else if(statement==ID_printf)
3667 else if(statement==ID_nondet)
3669 else if(statement==
"prob_coin")
3671 else if(statement==
"prob_unif")
3673 else if(statement==ID_statement_expression)
3675 else if(statement == ID_va_start)
3681 else if(src.
id()==ID_literal)
3684 else if(src.
id()==ID_not)
3687 else if(src.
id()==ID_bitnot)
3690 else if(src.
id()==ID_mult)
3693 else if(src.
id()==ID_div)
3696 else if(src.
id()==ID_mod)
3699 else if(src.
id()==ID_shl)
3702 else if(src.
id()==ID_ashr || src.
id()==ID_lshr)
3705 else if(src.
id()==ID_lt || src.
id()==ID_gt ||
3706 src.
id()==ID_le || src.
id()==ID_ge)
3712 else if(src.
id()==ID_notequal)
3715 else if(src.
id()==ID_equal)
3718 else if(src.
id()==ID_ieee_float_equal)
3721 else if(src.
id()==ID_width)
3724 else if(src.
id()==ID_concatenation)
3727 else if(src.
id()==ID_ieee_float_notequal)
3730 else if(src.
id()==ID_abs)
3733 else if(src.
id()==ID_complex_real)
3736 else if(src.
id()==ID_complex_imag)
3739 else if(src.
id()==ID_complex)
3742 else if(src.
id()==ID_bitand)
3745 else if(src.
id()==ID_bitxor)
3748 else if(src.
id()==ID_bitor)
3751 else if(src.
id()==ID_and)
3754 else if(src.
id()==ID_or)
3757 else if(src.
id()==ID_xor)
3760 else if(src.
id()==ID_implies)
3763 else if(src.
id()==ID_if)
3766 else if(src.
id()==ID_forall)
3770 else if(src.
id()==ID_exists)
3774 else if(src.
id()==ID_lambda)
3778 else if(src.
id()==ID_with)
3781 else if(src.
id()==ID_update)
3784 else if(src.
id()==ID_member_designator)
3787 else if(src.
id()==ID_index_designator)
3790 else if(src.
id()==ID_symbol)
3793 else if(src.
id()==ID_next_symbol)
3796 else if(src.
id()==ID_nondet_symbol)
3799 else if(src.
id()==ID_predicate_symbol)
3802 else if(src.
id()==ID_predicate_next_symbol)
3805 else if(src.
id()==ID_predicate_passive_symbol)
3808 else if(src.
id()==
"quant_symbol")
3811 else if(src.
id()==ID_nondet_bool)
3814 else if(src.
id()==ID_object_descriptor)
3817 else if(src.
id()==
"Hoare")
3820 else if(src.
id()==ID_code)
3823 else if(src.
id()==ID_constant)
3826 else if(src.
id()==ID_string_constant)
3830 else if(src.
id()==ID_struct)
3833 else if(src.
id()==ID_vector)
3836 else if(src.
id()==ID_union)
3839 else if(src.
id()==ID_array)
3842 else if(src.
id() == ID_array_list)
3845 else if(src.
id()==ID_typecast)
3848 else if(src.
id()==ID_comma)
3851 else if(src.
id()==ID_ptr_object)
3852 return "PTR_OBJECT("+
id2string(src.
get(ID_identifier))+
")";
3854 else if(src.
id()==ID_cond)
3858 src.
id() == ID_overflow_unary_minus || src.
id() == ID_overflow_minus ||
3859 src.
id() == ID_overflow_mult || src.
id() == ID_overflow_plus ||
3860 src.
id() == ID_overflow_shl)
3865 else if(src.
id()==ID_unknown)
3868 else if(src.
id()==ID_invalid)
3871 else if(src.
id()==ID_extractbit)
3874 else if(src.
id()==ID_extractbits)
3877 else if(src.
id()==ID_initializer_list ||
3878 src.
id()==ID_compound_literal)
3884 else if(src.
id()==ID_designated_initializer)
3890 else if(src.
id()==ID_sizeof)
3893 else if(src.
id()==ID_let)
3896 else if(src.
id()==ID_type)
3905 unsigned precedence;
3916 const std::string &identifier)
3928 expr2c.get_shorthands(expr);
3929 return expr2c.convert(expr);
3944 return expr2c.convert(type);
3954 const std::string &identifier,
3959 return expr2c.convert_with_identifier(type, identifier);
std::string MetaString(const std::string &in)
virtual void read(const typet &src) override
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
void irep2lisp(const irept &src, lispexprt &dest)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const exprt & case_op() const
const irep_idt & get_function() const
const irep_idt & get_comment() const
bool has_ellipsis() const
std::string convert_code_while(const code_whilet &src, unsigned indent)
A codet representing sequential composition of program statements.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const char * c_str() const
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const typet & subtype() const
codet representation of a switch-case, i.e. a case statement within a switch.
std::string convert_code_fence(const codet &src, unsigned indent)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
std::string convert_cond(const exprt &src, unsigned precedence)
bool can_cast_expr< code_inputt >(const exprt &base)
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
const exprt & cond() const
codet representing a while statement.
Expression to hold a nondeterministic choice.
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
std::string convert_union(const exprt &src, unsigned &precedence)
bool print_enum_int_value
When printing an enum-typed constant, print the integer representation.
codet representation of an inline assembler statement.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
codet representation of a for statement.
const irep_idt & get_identifier() const
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
The type of an expression, extends irept.
const irept::named_subt & get_pragmas() const
std::vector< parametert > parameterst
static std::string clean_identifier(const irep_idt &id)
const codet & then_case() const
An expression with three operands.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::string convert_comma(const exprt &src, unsigned precedence)
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bool use_library_macros
This is the string that will be printed for null pointers.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
std::string convert_code_assert(const codet &src, unsigned indent)
Base type for structs and unions.
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...
typet type
Type of symbol.
floatbv_typet long_double_type()
std::string to_ansi_c_string() const
A side_effect_exprt representation of a function call side effect.
std::unordered_set< irep_idt > find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol.
std::string convert_quantifier(const quantifier_exprt &, const std::string &symbol, unsigned precedence)
std::vector< c_enum_membert > memberst
bool is_signed(const typet &t)
Convenience function – is the type signed?
Various predicates over pointers in programs.
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
std::string convert_update(const update_exprt &, unsigned precedence)
std::string convert_let(const let_exprt &, unsigned precedence)
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
const irept & find(const irep_namet &name) const
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string convert_code_decl(const codet &src, unsigned indent)
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
std::string convert_code_decl_block(const codet &src, unsigned indent)
std::string convert_nondet_bool()
const string_constantt & to_string_constant(const exprt &expr)
std::string convert_code_expression(const codet &src, unsigned indent)
Base class for all expressions.
const exprt & iter() const
std::string convert_quantified_symbol(const exprt &src)
std::vector< componentt > componentst
Generic base class for unary expressions.
std::string convert_array_list(const exprt &src, unsigned &precedence)
A base class for binary expressions.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
irep_idt base_name
Base (non-scoped) name.
A struct tag type, i.e., struct_typet with an identifier.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
static expr2c_configurationt default_configuration
This prints a human readable C like syntax that closely mirrors the internals of the GOTO program.
const code_whilet & to_code_while(const codet &code)
const irep_idt & get_pretty_name() const
std::string convert_code_input(const codet &src, unsigned indent)
A base class for quantifier expressions.
const exprt & cond() const
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
std::string convert_Hoare(const exprt &src)
std::string convert_code(const codet &src)
bool is_true() const
Return whether the expression is a constant representing true.
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
std::string convert_array_of(const exprt &src, unsigned precedence)
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
struct configt::ansi_ct ansi_c
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)
Expression to hold a symbol (variable)
bool has_suffix(const std::string &s, const std::string &suffix)
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_code_switch_case(const code_switch_caset &src, unsigned indent)
std::string convert_predicate_symbol(const exprt &src)
const code_fort & to_code_for(const codet &code)
std::unordered_map< irep_idt, irep_idt > shorthands
codet representation of an if-then-else statement.
A union tag type, i.e., union_typet with an identifier.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
std::string convert_trinary(const ternary_exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
const codet & to_code(const exprt &expr)
std::string convert_code_assign(const code_assignt &src, unsigned indent)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const code_switch_caset & to_code_switch_case(const codet &code)
std::string convert_overflow(const exprt &src, unsigned &precedence)
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
code_operandst & statements()
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
typet & type()
Return the type of the expression.
exprt & value()
convenience accessor for the value of a single binding
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
std::string convert_predicate_passive_symbol(const exprt &src)
std::size_t get_component_number() const
virtual std::string convert(const typet &src)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
codet representation of a do while statement.
std::string convert_code_array_set(const codet &src, unsigned indent)
std::string convert_code_for(const code_fort &src, unsigned indent)
std::string convert_member_designator(const exprt &src)
std::string convert_array_member_value(const exprt &src, unsigned precedence)
const exprt & init() const
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
signedbv_typet signed_int_type()
bool has_prefix(const std::string &s, const std::string &prefix)
std::string convert_nondet_symbol(const nondet_symbol_exprt &)
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
std::string convert_code_printf(const codet &src, unsigned indent)
std::string expr2string() const
bool has_operands() const
Return true if there is at least one operand.
const std::string & id2string(const irep_idt &d)
static std::string indent_str(unsigned indent)
const exprt & compound() const
std::string to_ansi_c_string() const
#define forall_operands(it, expr)
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
#define SYMEX_DYNAMIC_PREFIX
std::string convert_function(const exprt &src, const std::string &symbol)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
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.
const code_ifthenelset & to_code_ifthenelse(const codet &code)
codet representation of a label for branch targets.
virtual std::unique_ptr< qualifierst > clone() const =0
const irep_idt & get_identifier() const
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
bitvector_typet wchar_t_type()
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
const code_labelt & to_code_label(const codet &code)
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
floatbv_typet float_type()
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
API to expression classes for Pointers.
bool include_struct_padding_components
When printing struct_typet or struct_exprt, include the artificial padding components introduced to k...
std::string convert_code_asm(const code_asmt &src, unsigned indent)
const std::string & id_string() const
Application of (mathematical) function.
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
std::size_t long_long_int_width
const code_dowhilet & to_code_dowhile(const codet &code)
std::string convert_code_lock(const codet &src, unsigned indent)
std::string convert_code_label(const code_labelt &src, unsigned indent)
std::string convert_unary(const unary_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_extractbits(const extractbits_exprt &src, unsigned precedence)
unsignedbv_typet unsigned_int_type()
std::string convert_array(const exprt &src)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const exprt & cond() const
std::string convert_code_goto(const codet &src, unsigned indent)
virtual std::string convert_symbol(const exprt &src)
const codet & body() const
const irep_idt & id() const
std::string convert_predicate_next_symbol(const exprt &src)
std::string convert_index(const exprt &src, unsigned precedence)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::string convert_byte_update(const byte_update_exprt &, unsigned precedence)
const code_function_callt & to_code_function_call(const codet &code)
std::vector< exprt > operandst
std::string convert_code_assume(const codet &src, unsigned indent)
const code_returnt & to_code_return(const codet &code)
API to expression classes for floating-point arithmetic.
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
std::string convert_initializer_list(const exprt &src)
const parameterst & parameters() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src)
const expr2c_configurationt & configuration
const constant_exprt & size() const
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Operator to update elements in structs and arrays.
std::string convert_code_continue(unsigned indent)
std::string convert_code_break(unsigned indent)
floatbv_typet double_type()
std::string convert_code_array_copy(const codet &src, unsigned indent)
std::string convert_extractbit(const extractbit_exprt &, unsigned precedence)
bitvector_typet char_type()
std::size_t get_width() const
const irep_idt & get_label() const
std::string convert_norep(const exprt &src, unsigned &precedence)
std::string convert_literal(const exprt &src)
code_asmt & to_code_asm(codet &code)
Extract member of struct or union.
const std::string & get_string(const irep_namet &name) const
std::string convert_function_application(const function_application_exprt &src)
std::string convert_with(const exprt &src, unsigned precedence)
bool can_cast_expr< code_outputt >(const exprt &base)
Structure type, corresponds to C style structs.
C enum tag type, i.e., c_enum_typet with an identifier.
std::string convert_code_block(const code_blockt &src, unsigned indent)
std::string c_type_as_string(const irep_idt &c_type)
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
std::size_t get_fraction_bits() const
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
std::string convert_code_array_replace(const codet &src, unsigned indent)
bool print_struct_body_in_type
When printing a struct_typet, should the components of the struct be printed inline.
const code_assignt & to_code_assign(const codet &code)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const irep_idt & get(const irep_namet &name) const
std::string convert_code_unlock(const codet &src, unsigned indent)
source_locationt location
Source code location of definition of symbol.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
std::string convert_nondet(const exprt &src, unsigned &precedence)
void get_shorthands(const exprt &expr)
const codet & body() const
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
exprt::operandst & arguments()
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const codet & body() const
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
const codet & else_case() const
std::size_t long_double_width
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::string convert_sizeof(const exprt &src, unsigned &precedence)
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.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
std::size_t short_int_width
irep_idt id_shorthand(const irep_idt &identifier) const
const exprt & cond() const
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const typet & return_type() const
const code_blockt & to_code_block(const codet &code)
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string convert_code_dead(const codet &src, unsigned indent)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool include_array_size
When printing array_typet, should the size of the array be printed.
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
#define forall_expr(it, expr)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
std::string convert_index_designator(const exprt &src)
Used for configuring the behaviour of expr2c and type2c.
const irep_idt & get_flavor() const
Semantic type conversion.
std::string convert_code_switch(const codet &src, unsigned indent)
unsignedbv_typet size_type()
std::string convert_member(const member_exprt &src, unsigned precedence)
A codet representing an assignment in the program.
const irep_idt & get_statement() const
A constant literal expression.
std::string true_string
This is the string that will be printed for the true boolean expression.
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
virtual std::string as_string() const override
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
exprt & where()
convenience accessor for binding().where()
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const irep_idt & get_value() const
const source_locationt & source_location() const
bool is_incomplete() const
A struct/union may be incomplete.
std::string convert_complex(const exprt &src, unsigned precedence)
std::string convert_code_output(const codet &src, unsigned indent)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
bool expand_typedef
Print the expanded type instead of a typedef name, even when a typedef is present.
std::string convert_designated_initializer(const exprt &src)
std::string convert_vector(const exprt &src, unsigned &precedence)
std::string convert_binary(const binary_exprt &, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string false_string
This is the string that will be printed for the false boolean expression.
std::size_t long_int_width
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const memberst & members() const
std::string convert_allocate(const exprt &src, unsigned &precedence)
std::string convert_code_return(const codet &src, unsigned indent)
Data structure for representing an arbitrary statement in a program.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)