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);
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_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 shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
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()
A base class for binary expressions.
std::size_t get_width() const
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
C enum tag type, i.e., c_enum_typet with an identifier.
const memberst & members() const
std::vector< c_enum_membert > memberst
virtual std::string as_string() const override
virtual void read(const typet &src) override
codet representation of an inline assembler statement.
const irep_idt & get_flavor() const
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
code_operandst & statements()
codet representation of a do while statement.
const exprt & cond() const
const codet & body() const
codet representation of a for statement.
const exprt & init() const
const exprt & iter() const
const exprt & cond() const
const codet & body() const
codet representation of a function call statement.
codet representation of an if-then-else statement.
const codet & then_case() const
const exprt & cond() const
const codet & else_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 typet & return_type() const
bool has_ellipsis() const
const parameterst & parameters() 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
struct configt::ansi_ct ansi_c
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
std::string convert_nondet(const exprt &src, unsigned &precedence)
std::string convert_literal(const exprt &src)
std::string convert_code_continue(unsigned indent)
virtual std::string convert_array_type(const typet &src, const qualifierst &qualifiers, const std::string &declarator_str)
To generate a C-like type declaration of an array.
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
std::string convert_comma(const exprt &src, unsigned precedence)
std::string convert_code_assert(const codet &src, unsigned indent)
std::string convert_quantifier(const quantifier_exprt &, const std::string &symbol, unsigned precedence)
std::string convert_union(const exprt &src, unsigned &precedence)
std::string convert_code_expression(const codet &src, unsigned indent)
std::string convert_code_goto(const codet &src, unsigned indent)
std::string convert_code_switch(const codet &src, unsigned indent)
std::string convert_initializer_list(const exprt &src)
std::string convert_quantified_symbol(const exprt &src)
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_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_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_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_code_decl(const codet &src, unsigned indent)
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_member_designator(const exprt &src)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
std::string convert_byte_extract(const byte_extract_exprt &, unsigned precedence)
std::string convert_code_label(const code_labelt &src, unsigned indent)
virtual std::string convert_symbol(const exprt &src)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
std::string convert_code_array_copy(const codet &src, unsigned indent)
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
std::string convert_code_dead(const codet &src, unsigned indent)
virtual std::string convert_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_assign(const code_assignt &src, unsigned indent)
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
std::string convert_code_fence(const codet &src, unsigned indent)
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_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_index(const exprt &src, unsigned precedence)
std::string convert_code_assume(const codet &src, unsigned indent)
std::string convert_code_input(const codet &src, unsigned indent)
std::string convert_extractbit(const extractbit_exprt &, unsigned precedence)
std::string convert_predicate_next_symbol(const exprt &src)
std::string convert_code_array_set(const codet &src, unsigned indent)
std::string convert_function(const exprt &src, const std::string &symbol)
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_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.
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
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.
const std::string & get_string(const irep_namet &name) const
bool get_bool(const irep_namet &name) const
const irept & find(const irep_namet &name) const
const std::string & id_string() const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
exprt & where()
convenience accessor for binding().where()
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
exprt & value()
convenience accessor for the value of a single binding
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
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a nondeterministic choice.
const irep_idt & get_identifier() const
virtual std::unique_ptr< qualifierst > clone() const =0
A base class for quantifier expressions.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
const irep_idt & get_function() const
const irep_idt & get_comment() const
const irept::named_subt & get_pragmas() 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 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.
const componentst & components() const
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
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.
Semantic type conversion.
The type of an expression, extends irept.
const typet & subtype() const
Generic base class for unary expressions.
A union tag type, i.e., union_typet with an identifier.
Operator to update elements in structs and arrays.
const constant_exprt & size() const
bool has_prefix(const std::string &s, const std::string &prefix)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
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)
std::unordered_set< irep_idt > find_symbol_identifiers(const exprt &src)
Find identifiers of the sub expressions with id ID_symbol.
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 std::string & id2string(const irep_idt &d)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void irep2lisp(const irept &src, lispexprt &dest)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
optionalt< exprt > build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
#define UNREACHABLE
This should be used to mark dead code.
const code_ifthenelset & to_code_ifthenelse(const codet &code)
const code_returnt & to_code_return(const codet &code)
bool can_cast_expr< code_inputt >(const exprt &base)
const code_whilet & to_code_while(const codet &code)
const code_switch_caset & to_code_switch_case(const codet &code)
bool can_cast_expr< code_outputt >(const exprt &base)
const code_labelt & to_code_label(const codet &code)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const codet & to_code(const exprt &expr)
const code_dowhilet & to_code_dowhile(const codet &code)
const code_blockt & to_code_block(const codet &code)
const code_fort & to_code_for(const codet &code)
const code_function_callt & to_code_function_call(const codet &code)
code_asmt & to_code_asm(codet &code)
const code_assignt & to_code_assign(const codet &code)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_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 not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
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 vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const string_constantt & to_string_constant(const exprt &expr)
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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.
std::size_t long_double_width
std::size_t long_long_int_width
std::size_t long_int_width
std::size_t short_int_width
Used for configuring the behaviour of expr2c and type2c.
bool print_enum_int_value
When printing an enum-typed constant, print the integer representation.
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
bool expand_typedef
Print the expanded type instead of a typedef name, even when a typedef is present.
static expr2c_configurationt default_configuration
This prints a human readable C like syntax that closely mirrors the internals of the GOTO program.
std::string true_string
This is the string that will be printed for the true boolean expression.
bool print_struct_body_in_type
When printing a struct_typet, should the components of the struct be printed inline.
bool use_library_macros
This is the string that will be printed for null pointers.
bool include_struct_padding_components
When printing struct_typet or struct_exprt, include the artificial padding components introduced to k...
std::string false_string
This is the string that will be printed for the false boolean expression.
bool include_array_size
When printing array_typet, should the size of the array be printed.
bool has_suffix(const std::string &s, const std::string &suffix)
bool is_signed(const typet &t)
Convenience function – is the type signed?