Go to the documentation of this file.
78 if(
pos!=std::string::npos)
89 if(c_pos!=std::string::npos &&
90 dest.rfind(
"::")==c_pos)
91 dest.erase(0, c_pos+2);
92 else if(c_pos!=std::string::npos)
94 for(std::string::iterator it2=dest.begin();
115 for(find_symbols_sett::const_iterator
129 func = func.substr(0, func.rfind(
"::"));
139 if(!
shorthands.insert(std::make_pair(*it, sh)).second)
143 for(find_symbols_sett::const_iterator
162 has_collision=!
ns.
lookup(sh, symbol);
191 const std::string &declarator)
193 std::unique_ptr<qualifierst> clone = qualifiers.
clone();
194 c_qualifierst &new_qualifiers = dynamic_cast<c_qualifierst &>(*clone);
195 new_qualifiers.
read(src);
197 std::string q=new_qualifiers.
as_string();
200 declarator==
""?declarator:
" "+declarator;
207 if(src.
id()==ID_bool)
211 else if(src.
id()==ID_c_bool)
215 else if(src.
id()==ID_string)
219 else if(src.
id()==ID_natural ||
220 src.
id()==ID_integer ||
221 src.
id()==ID_rational)
225 else if(src.
id()==ID_empty)
229 else if(src.
id()==ID_complex)
234 else if(src.
id()==ID_floatbv)
243 return q+
"long double"+d;
248 return q +
CPROVER_PREFIX +
"floatbv[" + swidth +
"][" + fwidth +
"]";
251 else if(src.
id()==ID_fixedbv)
259 else if(src.
id()==ID_c_bit_field)
264 else if(src.
id()==ID_signedbv ||
265 src.
id()==ID_unsignedbv)
271 if(c_type==ID_char &&
274 if(src.
id()==ID_signedbv)
275 return q+
"signed char"+d;
277 return q+
"unsigned char"+d;
279 else if(c_type!=ID_wchar_t && !c_type_str.
empty())
280 return q+c_type_str+d;
287 std::string sign_str=
is_signed?
"signed ":
"unsigned ";
293 return q+sign_str+
"int"+d;
299 return q+sign_str+
"long int"+d;
304 return q+sign_str+
"char"+d;
310 return q+sign_str+
"short int"+d;
316 return q+sign_str+
"long long int"+d;
322 return q+sign_str+
"__int128";
330 else if(src.
id()==ID_struct)
334 else if(src.
id()==ID_incomplete_struct)
336 std::string dest=q+
"struct";
338 const std::string &tag=src.
get_string(ID_tag);
345 else if(src.
id()==ID_union)
349 std::string dest=q+
"union";
369 else if(src.
id()==ID_incomplete_union)
371 std::string dest=q+
"union";
373 const std::string &tag=src.
get_string(ID_tag);
380 else if(src.
id()==ID_c_enum)
404 for(c_enum_typet::memberst::const_iterator
409 if(it!=members.begin())
422 else if(src.
id()==ID_incomplete_c_enum)
428 std::string result=q+
"enum";
434 else if(src.
id()==ID_c_enum_tag)
438 std::string result=q+
"enum";
443 else if(src.
id()==ID_pointer)
450 std::string new_declarator=
"*";
453 (!declarator.empty() || subtype_followed.
id()==ID_pointer))
454 new_declarator+=
" "+q;
456 new_declarator+=declarator;
459 if(subtype_followed.
id()==ID_code ||
461 (subtype_followed.
id()==ID_array ||
462 subtype_followed.
id()==ID_incomplete_array)))
463 new_declarator=
"("+new_declarator+
")";
467 else if(src.
id()==ID_array)
471 else if(src.
id()==ID_incomplete_array)
476 src.
subtype(), qualifiers, declarator+
"[]");
478 else if(src.
id() == ID_symbol_type)
481 const irep_idt &typedef_identifer=symbolic_type.
get(ID_typedef);
485 if(typedef_identifer!=
"")
493 if(followed.
id()==ID_struct)
495 std::string dest=q+
"struct";
502 else if(followed.
id()==ID_union)
504 std::string dest=q+
"union";
512 return convert_rec(followed, new_qualifiers, declarator);
515 else if(src.
id()==ID_struct_tag)
520 std::string dest=q+
"struct";
528 else if(src.
id()==ID_union_tag)
533 std::string dest=q+
"union";
541 else if(src.
id()==ID_code)
547 std::string dest=declarator+
"(";
551 if(parameters.empty())
560 for(code_typet::parameterst::const_iterator
561 it=parameters.begin();
562 it!=parameters.end();
565 if(it!=parameters.begin())
568 if(it->get_identifier().empty())
572 std::string arg_declarator=
598 while(non_ptr_type->
id()==ID_pointer)
601 if(non_ptr_type->
id()==ID_code ||
602 non_ptr_type->
id()==ID_array)
603 dest=
convert_rec(return_type, ret_qualifiers, dest);
605 dest=
convert_rec(return_type, ret_qualifiers,
"")+
" "+dest;
611 if(dest[dest.size()-1]==
' ')
612 dest.resize(dest.size()-1);
617 else if(src.
id()==ID_vector)
621 const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.
size());
626 if(tmp==
"signed char" || tmp==
"char")
628 else if(tmp==
"signed short int")
630 else if(tmp==
"signed int")
632 else if(tmp==
"signed long long int")
634 else if(tmp==
"float")
636 else if(tmp==
"double")
642 dest+=
" __attribute__((vector_size (";
644 dest+=
"*sizeof("+subtype+
"))))";
649 else if(src.
id()==ID_gcc_builtin_va_list)
651 return q+
"__builtin_va_list"+d;
653 else if(src.
id()==ID_constructor ||
654 src.
id()==ID_destructor)
656 return q+
"__attribute__(("+
id2string(src.
id())+
")) void"+d;
677 const std::string &qualifiers_str,
678 const std::string &declarator_str)
700 const std::string &qualifiers,
701 const std::string &declarator,
702 bool inc_struct_body,
703 bool inc_padding_components)
708 assert(inc_struct_body || !inc_padding_components);
712 std::string dest=qualifiers+
"struct";
725 if(
component.get_is_padding() && !inc_padding_components)
755 const std::string &declarator_str)
772 const std::string &declarator_str,
773 bool inc_size_if_possible)
776 std::string array_suffix;
778 if(
to_array_type(src).size().is_nil() || !inc_size_if_possible)
786 src.
subtype(), qualifiers, declarator_str+array_suffix);
791 unsigned &precedence)
801 if(to_type.
id()==ID_c_bool &&
805 if(to_type.
id()==ID_bool &&
825 const std::string &symbol1,
826 const std::string &symbol2,
875 const std::string &symbol,
886 std::string dest=symbol+
" { ";
915 for(
size_t i=1; i<src.
operands().size(); i+=2)
917 std::string op1, op2;
923 if(src.
operands()[i].id()==ID_member_name)
926 src.
operands()[i].get(ID_component_name);
941 display_component_name=component_name;
945 op1=
"."+
id2string(display_component_name);
973 std::string dest=
"LET ";
995 std::string op0, op1, op2;
1029 unsigned precedence)
1034 bool condition=
true;
1036 std::string dest=
"cond {\n";
1053 condition=!condition;
1063 const std::string &symbol,
1064 unsigned precedence,
1065 bool full_parentheses)
1087 bool use_parentheses0=
1089 (precedence==p0 && full_parentheses) ||
1090 (precedence==p0 && src.
id()!=op0.
id());
1092 if(use_parentheses0)
1095 if(use_parentheses0)
1102 bool use_parentheses1=
1104 (precedence==p1 && full_parentheses) ||
1105 (precedence==p1 && src.
id()!=op1.
id());
1107 if(use_parentheses1)
1110 if(use_parentheses1)
1118 const std::string &symbol,
1119 unsigned precedence,
1120 bool full_parentheses)
1150 bool use_parentheses=
1152 (precedence==p && full_parentheses) ||
1153 (precedence==p && src.
id()!=it->id());
1167 const std::string &symbol,
1168 unsigned precedence)
1176 std::string dest=symbol;
1199 std::string dest =
"ALLOCATE";
1202 if(src.
type().
id()==ID_pointer &&
1209 dest += op0 +
", " + op1;
1217 unsigned &precedence)
1227 unsigned &precedence)
1230 to_code(src.
op0()).get_statement()!=ID_block)
1238 unsigned &precedence)
1248 unsigned &precedence)
1255 unsigned &precedence)
1265 const std::string &name,
1266 unsigned precedence)
1268 std::string dest=name;
1289 unsigned precedence)
1296 if(*op0.rbegin()==
';')
1297 op0.resize(op0.size()-1);
1301 if(*op1.rbegin()==
';')
1302 op1.resize(op1.size()-1);
1304 std::string dest=op0;
1313 unsigned precedence)
1317 src.
op1().
id()==ID_constant)
1329 const typet &subtype=
1343 std::string dest=name;
1364 unsigned precedence)
1374 unsigned precedence)
1399 unsigned precedence)
1429 const std::string &symbol,
1430 unsigned precedence)
1451 unsigned precedence)
1474 const exprt &src,
unsigned &precedence)
1479 std::string dest=
"POINTER_ARITHMETIC(";
1511 const exprt &src,
unsigned &precedence)
1516 std::string dest=
"POINTER_DIFFERENCE(";
1549 unsigned precedence;
1554 return "."+src.
get_string(ID_component_name);
1559 unsigned precedence;
1569 unsigned precedence)
1577 if(src.
op0().
id()==ID_dereference &&
1582 if(precedence>p || src.
op0().
op0().
id()==ID_typecast)
1585 if(precedence>p || src.
op0().
op0().
id()==ID_typecast)
1594 if(precedence>p || src.
op0().
id()==ID_typecast)
1597 if(precedence>p || src.
op0().
id()==ID_typecast)
1605 if(full_type.
id()!=ID_struct &&
1606 full_type.
id()!=ID_union)
1614 if(component_name!=
"")
1616 const exprt comp_expr=
1622 if(!comp_expr.
get(ID_pretty_name).
empty())
1635 const exprt comp_expr=
1645 unsigned precedence)
1655 unsigned precedence)
1665 unsigned &precedence)
1676 unsigned &precedence)
1682 src.
op0().
id()==ID_predicate_passive_symbol)
1686 std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
1710 if(src.
id()==ID_next_symbol)
1711 dest=
"NEXT("+dest+
")";
1718 unsigned &precedence)
1721 return "nondet_symbol("+
id2string(
id)+
")";
1726 unsigned &precedence)
1728 const std::string &
id=src.
get_string(ID_identifier);
1729 return "ps("+
id+
")";
1734 unsigned &precedence)
1736 const std::string &
id=src.
get_string(ID_identifier);
1737 return "pns("+
id+
")";
1742 unsigned &precedence)
1744 const std::string &
id=src.
get_string(ID_identifier);
1745 return "pps("+
id+
")";
1750 unsigned &precedence)
1752 const std::string &
id=src.
get_string(ID_identifier);
1758 unsigned &precedence)
1760 return "nondet_bool()";
1765 unsigned &precedence)
1770 std::string result=
"<";
1789 unsigned &precedence)
1796 if(type.
id()==ID_integer ||
1797 type.
id()==ID_natural ||
1798 type.
id()==ID_rational)
1802 else if(type.
id()==ID_c_enum ||
1803 type.
id()==ID_c_enum_tag)
1809 if(c_enum_type.
id()!=ID_c_enum)
1823 for(c_enum_typet::memberst::const_iterator
1828 if(it->get_value()==int_value_string)
1829 return "/*enum*/"+
id2string(it->get_base_name());
1835 else if(type.
id()==ID_rational)
1837 else if(type.
id()==ID_bv)
1842 else if(type.
id()==ID_bool)
1846 else if(type.
id()==ID_unsignedbv ||
1847 type.
id()==ID_signedbv ||
1848 type.
id()==ID_c_bit_field ||
1849 type.
id()==ID_c_bool)
1857 type.
id()==ID_c_bit_field?type.
subtype().
get(ID_C_c_type):
1858 type.
get(ID_C_c_type);
1860 if(type.
id()==ID_c_bool)
1870 else if(int_value==
'\r')
1872 else if(int_value==
'\t')
1874 else if(int_value==
'\'')
1876 else if(int_value==
'\\')
1878 else if(int_value>=
' ' && int_value<126)
1898 if(c_type==ID_unsigned_int)
1900 else if(c_type==ID_unsigned_long_int)
1902 else if(c_type==ID_signed_long_int)
1904 else if(c_type==ID_unsigned_long_long_int)
1906 else if(c_type==ID_signed_long_long_int)
1917 dest=
convert(sizeof_expr)+
" /*"+dest+
"*/ ";
1923 else if(type.
id()==ID_floatbv)
1927 if(dest!=
"" && isdigit(dest[dest.size()-1]))
1929 if(dest.find(
'.')==std::string::npos)
1939 else if(dest.size()==4 &&
1940 (dest[0]==
'+' || dest[0]==
'-'))
1944 else if(dest==
"-inf")
1946 else if(dest==
"+NaN")
1948 else if(dest==
"-NaN")
1952 else if(type.
id()==ID_fixedbv)
1956 if(dest!=
"" && isdigit(dest[dest.size()-1]))
1964 else if(type.
id()==ID_array ||
1965 type.
id()==ID_incomplete_array)
1969 else if(type.
id()==ID_pointer)
1975 dest=
"(("+
convert(type)+
")"+dest+
")";
1977 else if(value==std::string(value.
size(),
'0') &&
1982 dest=
"(("+
convert(type)+
")"+dest+
")";
1990 if(src.
op0().
id()==ID_constant)
1994 if(op_value==
"INVALID" ||
1996 op_value==
"NULL+offset")
2005 else if(type.
id()==ID_string)
2029 unsigned &precedence)
2045 unsigned &precedence,
2046 bool include_padding_components)
2050 if(full_type.
id()!=ID_struct)
2059 if(components.size()!=src.
operands().size())
2062 std::string dest=
"{ ";
2064 exprt::operandst::const_iterator o_it=src.
operands().begin();
2072 if(o_it->type().id()==ID_code)
2075 if(
component.get_is_padding() && !include_padding_components)
2093 std::string tmp=
convert(*o_it);
2095 if(last_size+40<dest.size())
2098 last_size=dest.size();
2118 unsigned &precedence)
2122 if(full_type.
id()!=ID_vector)
2125 std::string dest=
"{ ";
2147 if(last_size+40<dest.size())
2150 last_size=dest.size();
2165 unsigned &precedence)
2167 std::string dest=
"{ ";
2186 unsigned &precedence)
2195 bool all_constant=
true;
2198 if(!it->is_constant())
2201 if(src.
get_bool(ID_C_string_constant) &&
2212 dest.reserve(dest.size()+1+src.
operands().size());
2214 bool last_was_hex=
false;
2222 const unsigned int ch = numeric_cast_v<unsigned>(*it);
2235 case '\n': dest+=
"\\n";
break;
2236 case '\t': dest+=
"\\t";
break;
2237 case '\v': dest+=
"\\v";
break;
2238 case '\b': dest+=
"\\b";
break;
2239 case '\r': dest+=
"\\r";
break;
2240 case '\f': dest+=
"\\f";
break;
2241 case '\a': dest+=
"\\a";
break;
2242 case '\\': dest+=
"\\\\";
break;
2243 case '"': dest+=
"\\\"";
break;
2246 if(ch>=
' ' && ch!=127 && ch<0xff)
2247 dest+=static_cast<char>(ch);
2250 std::ostringstream oss;
2251 oss <<
"\\x" << std::hex << ch;
2269 if(it->is_not_nil())
2289 unsigned &precedence)
2291 std::string dest=
"{ ";
2298 std::string tmp1=
convert(*it);
2302 std::string tmp2=
convert(*it);
2304 std::string tmp=
"["+tmp1+
"]="+tmp2;
2323 unsigned &precedence)
2326 if(src.
id()!=ID_compound_literal)
2343 if(src.
id()!=ID_compound_literal)
2351 unsigned &precedence)
2355 unsigned precedence;
2359 std::string dest=
".";
2369 unsigned &precedence)
2399 unsigned &precedence)
2429 unsigned &precedence)
2433 std::string dest=
"overflow(\"";
2460 return std::string(indent,
' ');
2475 if(!src.
operands()[1].operands().empty() ||
2476 !src.
operands()[2].operands().empty() ||
2477 !src.
operands()[3].operands().empty() ||
2478 !src.
operands()[4].operands().empty())
2486 if(it->operands().size()==2)
2501 if(it->operands().size()==2)
2518 if(it->id()==ID_gcc_asm_clobbered_register)
2547 unsigned precedence;
2573 unsigned precedence;
2602 unsigned precedence;
2640 unsigned precedence;
2684 unsigned precedence;
2700 const exprt &op=*it;
2702 if(op.
get(ID_statement)!=ID_block)
2704 unsigned precedence;
2740 unsigned precedence;
2748 const symbolt *symbol=
nullptr;
2759 dest +=
"__declspec(dllexport) ";
2762 if(symbol->
type.
id()==ID_code &&
2784 unsigned precedence;
2797 unsigned precedence;
2835 for(
const auto &statement : src.
statements())
2837 if(statement.get_statement() == ID_label)
2872 std::string expr_str;
2877 unsigned precedence;
2882 if(dest.empty() || *dest.rbegin()!=
';')
2892 static bool comment_done=
false;
2906 if(statement==ID_expression)
2909 if(statement==ID_block)
2912 if(statement==ID_switch)
2915 if(statement==ID_for)
2918 if(statement==ID_while)
2921 if(statement==ID_asm)
2924 if(statement==ID_skip)
2927 if(statement==ID_dowhile)
2930 if(statement==ID_ifthenelse)
2933 if(statement==ID_return)
2936 if(statement==ID_goto)
2939 if(statement==ID_printf)
2942 if(statement==ID_fence)
2945 if(statement==ID_input)
2948 if(statement==ID_output)
2951 if(statement==ID_assume)
2954 if(statement==ID_assert)
2957 if(statement==ID_break)
2960 if(statement==ID_continue)
2963 if(statement==ID_decl)
2966 if(statement==ID_decl_block)
2969 if(statement==ID_dead)
2972 if(statement==ID_assign)
2975 if(statement==
"lock")
2978 if(statement==
"unlock")
2981 if(statement==ID_atomic_begin)
2984 if(statement==ID_atomic_end)
2987 if(statement==ID_function_call)
2990 if(statement==ID_label)
2993 if(statement==ID_switch_case)
2996 if(statement==ID_array_set)
2999 if(statement==ID_array_copy)
3002 if(statement==ID_array_replace)
3005 if(statement==
"set_may" ||
3006 statement==
"set_must")
3010 unsigned precedence;
3031 unsigned precedence;
3044 unsigned precedence;
3057 unsigned precedence;
3088 if(it!=arguments.begin())
3103 std::string dest=
indent_str(indent)+
"printf(";
3125 std::string dest=
indent_str(indent)+
"FENCE(";
3128 { ID_WRfence, ID_RRfence, ID_RWfence, ID_WWfence,
3129 ID_RRcumul, ID_RWcumul, ID_WWcumul, ID_WRcumul,
3134 for(
unsigned i=0; !att[i].
empty(); i++)
3155 std::string dest=
indent_str(indent)+
"INPUT(";
3177 std::string dest=
indent_str(indent)+
"OUTPUT(";
3198 std::string dest=
indent_str(indent)+
"ARRAY_SET(";
3220 std::string dest=
indent_str(indent)+
"ARRAY_COPY(";
3242 std::string dest=
indent_str(indent)+
"ARRAY_REPLACE(";
3265 unsigned precedence;
3278 unsigned precedence;
3290 std::string labels_string;
3294 labels_string+=
"\n";
3297 labels_string+=
":\n";
3301 return labels_string+tmp;
3308 std::string labels_string;
3312 labels_string+=
"\n";
3314 labels_string+=
"default:\n";
3318 labels_string+=
"\n";
3320 labels_string+=
"case ";
3322 labels_string+=
":\n";
3325 unsigned next_indent=indent;
3331 return labels_string+tmp;
3341 unsigned precedence;
3349 static_cast<const codet &>(src.
find(ID_code));
3351 std::string dest=
"\n";
3356 std::string assumption_str=
convert(assumption);
3358 dest+=assumption_str;
3371 std::string assertion_str=
convert(assertion);
3373 dest+=assertion_str;
3384 unsigned precedence)
3399 unsigned precedence)
3416 unsigned &precedence)
3421 std::string dest=
"sizeof(";
3422 dest+=
convert(static_cast<const typet&>(src.
find(ID_type_arg)));
3430 unsigned &precedence)
3434 if(src.
id()==ID_plus)
3437 else if(src.
id()==ID_minus)
3440 else if(src.
id()==ID_unary_minus)
3443 else if(src.
id()==ID_unary_plus)
3446 else if(src.
id()==ID_floatbv_plus)
3449 else if(src.
id()==ID_floatbv_minus)
3452 else if(src.
id()==ID_floatbv_mult)
3455 else if(src.
id()==ID_floatbv_div)
3458 else if(src.
id()==ID_floatbv_rem)
3461 else if(src.
id()==ID_floatbv_typecast)
3464 std::string dest=
"FLOAT_TYPECAST(";
3493 else if(src.
id()==ID_sign)
3502 else if(src.
id()==ID_popcount)
3510 else if(src.
id() == ID_r_ok)
3513 else if(src.
id() == ID_w_ok)
3516 else if(src.
id()==ID_invalid_pointer)
3519 else if(src.
id()==ID_good_pointer)
3522 else if(src.
id()==ID_object_size)
3525 else if(src.
id()==
"pointer_arithmetic")
3528 else if(src.
id()==
"pointer_difference")
3531 else if(src.
id() == ID_null_object)
3532 return "NULL-object";
3534 else if(src.
id()==ID_integer_address ||
3535 src.
id()==ID_integer_address_object ||
3536 src.
id()==ID_stack_object ||
3537 src.
id()==ID_static_object)
3542 else if(src.
id()==ID_infinity)
3545 else if(src.
id()==
"builtin-function")
3548 else if(src.
id()==ID_pointer_object)
3551 else if(src.
id()==
"get_must")
3554 else if(src.
id()==
"get_may")
3557 else if(src.
id()==
"object_value")
3560 else if(src.
id()==ID_array_of)
3563 else if(src.
id()==ID_pointer_offset)
3566 else if(src.
id()==
"pointer_base")
3569 else if(src.
id()==
"pointer_cons")
3572 else if(src.
id()==ID_invalid_pointer)
3576 else if(src.
id()==ID_dynamic_object)
3579 else if(src.
id()==
"is_zero_string")
3582 else if(src.
id()==
"zero_string")
3585 else if(src.
id()==
"zero_string_length")
3588 else if(src.
id()==
"buffer_size")
3591 else if(src.
id()==ID_isnan)
3594 else if(src.
id()==ID_isfinite)
3597 else if(src.
id()==ID_isinf)
3600 else if(src.
id()==ID_bswap)
3607 else if(src.
id()==ID_isnormal)
3610 else if(src.
id()==ID_builtin_offsetof)
3613 else if(src.
id()==ID_gcc_builtin_va_arg)
3616 else if(src.
id()==ID_alignof)
3626 else if(src.
id()==ID_address_of)
3630 else if(src.
op0().
id()==ID_label)
3632 else if(src.
op0().
id()==ID_index &&
3641 else if(src.
id()==ID_dereference)
3645 else if(src.
type().
id()==ID_code)
3647 else if(src.
op0().
id()==ID_plus &&
3658 else if(src.
id()==ID_index)
3661 else if(src.
id()==ID_member)
3664 else if(src.
id()==
"array-member-value")
3667 else if(src.
id()==
"struct-member-value")
3670 else if(src.
id()==ID_function_application)
3675 else if(src.
id()==ID_side_effect)
3678 if(statement==ID_preincrement)
3680 else if(statement==ID_predecrement)
3682 else if(statement==ID_postincrement)
3684 else if(statement==ID_postdecrement)
3686 else if(statement==ID_assign_plus)
3688 else if(statement==ID_assign_minus)
3690 else if(statement==ID_assign_mult)
3692 else if(statement==ID_assign_div)
3694 else if(statement==ID_assign_mod)
3696 else if(statement==ID_assign_shl)
3698 else if(statement==ID_assign_shr)
3700 else if(statement==ID_assign_bitand)
3702 else if(statement==ID_assign_bitxor)
3704 else if(statement==ID_assign_bitor)
3706 else if(statement==ID_assign)
3708 else if(statement==ID_function_call)
3712 else if(statement == ID_allocate)
3714 else if(statement==ID_printf)
3716 else if(statement==ID_nondet)
3718 else if(statement==
"prob_coin")
3720 else if(statement==
"prob_unif")
3722 else if(statement==ID_statement_expression)
3724 else if(statement==ID_gcc_builtin_va_arg_next)
3730 else if(src.
id()==ID_literal)
3733 else if(src.
id()==ID_not)
3736 else if(src.
id()==ID_bitnot)
3739 else if(src.
id()==ID_mult)
3742 else if(src.
id()==ID_div)
3745 else if(src.
id()==ID_mod)
3748 else if(src.
id()==ID_shl)
3751 else if(src.
id()==ID_ashr || src.
id()==ID_lshr)
3754 else if(src.
id()==ID_lt || src.
id()==ID_gt ||
3755 src.
id()==ID_le || src.
id()==ID_ge)
3758 else if(src.
id()==ID_notequal)
3761 else if(src.
id()==ID_equal)
3764 else if(src.
id()==ID_ieee_float_equal)
3767 else if(src.
id()==ID_width)
3770 else if(src.
id()==ID_concatenation)
3773 else if(src.
id()==ID_ieee_float_notequal)
3776 else if(src.
id()==ID_abs)
3779 else if(src.
id()==ID_complex_real)
3782 else if(src.
id()==ID_complex_imag)
3785 else if(src.
id()==ID_complex)
3788 else if(src.
id()==ID_bitand)
3791 else if(src.
id()==ID_bitxor)
3794 else if(src.
id()==ID_bitor)
3797 else if(src.
id()==ID_and)
3800 else if(src.
id()==ID_or)
3803 else if(src.
id()==ID_xor)
3806 else if(src.
id()==ID_implies)
3809 else if(src.
id()==ID_if)
3812 else if(src.
id()==ID_forall)
3815 else if(src.
id()==ID_exists)
3818 else if(src.
id()==ID_lambda)
3821 else if(src.
id()==ID_with)
3824 else if(src.
id()==ID_update)
3827 else if(src.
id()==ID_member_designator)
3830 else if(src.
id()==ID_index_designator)
3833 else if(src.
id()==ID_symbol)
3836 else if(src.
id()==ID_next_symbol)
3839 else if(src.
id()==ID_nondet_symbol)
3842 else if(src.
id()==ID_predicate_symbol)
3845 else if(src.
id()==ID_predicate_next_symbol)
3848 else if(src.
id()==ID_predicate_passive_symbol)
3851 else if(src.
id()==
"quant_symbol")
3854 else if(src.
id()==ID_nondet_bool)
3857 else if(src.
id()==ID_object_descriptor)
3860 else if(src.
id()==
"Hoare")
3863 else if(src.
id()==ID_code)
3866 else if(src.
id()==ID_constant)
3869 else if(src.
id()==ID_string_constant)
3872 else if(src.
id()==ID_struct)
3875 else if(src.
id()==ID_vector)
3878 else if(src.
id()==ID_union)
3881 else if(src.
id()==ID_array)
3884 else if(src.
id() == ID_array_list)
3887 else if(src.
id()==ID_typecast)
3890 else if(src.
id()==ID_comma)
3893 else if(src.
id()==ID_ptr_object)
3894 return "PTR_OBJECT("+
id2string(src.
get(ID_identifier))+
")";
3896 else if(src.
id()==ID_cond)
3899 else if(src.
id()==ID_overflow_unary_minus ||
3900 src.
id()==ID_overflow_minus ||
3901 src.
id()==ID_overflow_mult ||
3902 src.
id()==ID_overflow_plus)
3905 else if(src.
id()==ID_unknown)
3908 else if(src.
id()==ID_invalid)
3911 else if(src.
id()==ID_extractbit)
3914 else if(src.
id()==ID_extractbits)
3917 else if(src.
id()==ID_initializer_list ||
3918 src.
id()==ID_compound_literal)
3921 else if(src.
id()==ID_designated_initializer)
3924 else if(src.
id()==ID_sizeof)
3927 else if(src.
id()==ID_let)
3930 else if(src.
id()==ID_type)
3939 unsigned precedence;
3950 const std::string &identifier)
3962 expr2c.get_shorthands(expr);
3963 return expr2c.convert(expr);
3978 return expr2c.convert(type);
3988 const std::string &identifier,
3993 return expr2c.convert_with_identifier(type, identifier);
std::string MetaString(const std::string &in)
virtual void read(const typet &src) override
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 char * c_str() const
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
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)
std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
std::string convert_cond(const exprt &src, unsigned precedence)
std::string convert_byte_update(const exprt &src, unsigned precedence)
const exprt & size() const
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)
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.
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.
std::vector< parametert > parameterst
static std::string clean_identifier(const irep_idt &id)
const codet & then_case() const
std::string convert_literal(const exprt &src, unsigned &precedence)
std::string convert_comma(const exprt &src, unsigned precedence)
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
std::string convert_quantified_symbol(const exprt &src, unsigned &precedence)
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 convert_array(const exprt &src, unsigned &precedence)
std::string to_ansi_c_string() const
A side_effect_exprt representation of a function call side effect.
mp_integer::ullong_t integer2ulong(const mp_integer &n)
std::vector< c_enum_membert > memberst
bool is_signed(const typet &t)
Convenience function – is the type signed?
const mp_integer string2integer(const std::string &n, unsigned base)
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_let(const let_exprt &, unsigned precedence)
std::string convert_unary(const exprt &src, const std::string &symbol, 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)
std::string convert_code_decl_block(const codet &src, unsigned indent)
std::string convert_code_expression(const codet &src, unsigned indent)
Base class for all expressions.
const exprt & iter() const
std::vector< componentt > componentst
std::string convert_array_list(const exprt &src, unsigned &precedence)
irep_idt base_name
Base (non-scoped) name.
A struct tag type, i.e., struct_typet with an identifier.
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.
std::string convert_initializer_list(const exprt &src, unsigned &precedence)
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)
struct configt::ansi_ct ansi_c
const exprt & cond() const
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string convert_function_application(const function_application_exprt &src, unsigned &precedence)
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)
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)
const code_fort & to_code_for(const codet &code)
#define UNREACHABLE
This should be used to mark dead code.
std::string convert_byte_extract(const exprt &src, unsigned precedence)
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.
exprt build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
const codet & to_code(const exprt &expr)
std::string convert_code_assign(const code_assignt &src, unsigned indent)
std::string convert_trinary(const exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
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
std::string convert_quantifier(const exprt &src, const std::string &symbol, unsigned precedence)
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.
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_code_break(const codet &src, unsigned indent)
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)
void find_symbols(const exprt &src, find_symbols_sett &dest)
std::string convert_code_continue(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()
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)
std::string to_ansi_c_string() const
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
#define forall_operands(it, expr)
std::string convert_binary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence)
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
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_update(const exprt &src, unsigned precedence)
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()
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.
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_nondet_bool(const exprt &src, unsigned &precedence)
unsignedbv_typet unsigned_int_type()
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)
const codet & body() const
const irep_idt & id() const
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.
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)
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
const parameterst & parameters() const
const expr2c_configurationt & configuration
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence)
floatbv_typet double_type()
std::string convert_code_array_copy(const codet &src, unsigned indent)
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)
bool is_zero() const
Return whether the expression is a constant representing 0.
code_asmt & to_code_asm(codet &code)
virtual std::string convert_symbol(const exprt &src, unsigned &precedence)
Extract member of struct or union.
const std::string & get_string(const irep_namet &name) const
std::string convert_with(const exprt &src, unsigned precedence)
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)
std::string convert_designated_initializer(const exprt &src, unsigned &precedence)
std::size_t get_fraction_bits() const
std::string convert_extractbits(const exprt &src, unsigned precedence)
std::unordered_set< irep_idt > find_symbols_sett
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 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.
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
symbol_exprt & function()
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.
std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence)
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 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.
bool has_prefix(const std::string &s, const std::string &prefix)
irep_idt get_component_name() const
Base class for tree-like data structures with sharing.
std::string convert_code_dead(const codet &src, unsigned indent)
A reference into the symbol table.
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_predicate_symbol(const exprt &src, unsigned &precedence)
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.
std::string convert_extractbit(const exprt &src, unsigned precedence)
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
virtual std::string as_string() const override
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
const irep_idt & get_value() const
const source_locationt & source_location() const
std::string convert_complex(const exprt &src, unsigned precedence)
std::string convert_code_output(const codet &src, unsigned indent)
std::string convert_vector(const exprt &src, unsigned &precedence)
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)