56 if(
pos!=std::string::npos)
67 if(c_pos!=std::string::npos &&
68 dest.rfind(
"::")==c_pos)
69 dest.erase(0, c_pos+2);
70 else if(c_pos!=std::string::npos)
72 for(std::string::iterator it2=dest.begin();
82 std::replace(dest.begin(), dest.end(),
'.',
'_');
93 for(find_symbols_sett::const_iterator
107 func = func.substr(0, func.rfind(
"::"));
117 if(!
shorthands.insert(std::make_pair(*it, sh)).second)
121 for(find_symbols_sett::const_iterator
140 has_collision=!
ns.
lookup(sh, symbol);
169 const std::string &declarator)
171 std::unique_ptr<qualifierst> clone = qualifiers.
clone();
173 new_qualifiers.
read(src);
175 std::string q=new_qualifiers.
as_string();
178 declarator==
""?declarator:
" "+declarator;
185 if(src.
id()==ID_bool)
189 else if(src.
id()==ID_c_bool)
193 else if(src.
id()==ID_string)
195 return q+
"__CPROVER_string"+d;
197 else if(src.
id()==ID_natural ||
198 src.
id()==ID_integer ||
199 src.
id()==ID_rational)
203 else if(src.
id()==ID_empty)
207 else if(src.
id()==ID_complex)
212 else if(src.
id()==ID_floatbv)
221 return q+
"long double"+d;
226 return q+
"__CPROVER_floatbv["+swidth+
"]["+fwidth+
"]";
229 else if(src.
id()==ID_fixedbv)
238 else if(src.
id()==ID_c_bit_field)
243 else if(src.
id()==ID_signedbv ||
244 src.
id()==ID_unsignedbv)
250 if(c_type==ID_char &&
253 if(src.
id()==ID_signedbv)
254 return q+
"signed char"+d;
256 return q+
"unsigned char"+d;
258 else if(c_type!=ID_wchar_t && !c_type_str.
empty())
259 return q+c_type_str+d;
266 std::string sign_str=
is_signed?
"signed ":
"unsigned ";
272 return q+sign_str+
"int"+d;
278 return q+sign_str+
"long int"+d;
283 return q+sign_str+
"char"+d;
289 return q+sign_str+
"short int"+d;
295 return q+sign_str+
"long long int"+d;
301 return q+sign_str+
"__int128";
309 else if(src.
id()==ID_struct)
313 else if(src.
id()==ID_incomplete_struct)
315 std::string dest=q+
"struct";
317 const std::string &tag=src.
get_string(ID_tag);
324 else if(src.
id()==ID_union)
328 std::string dest=q+
"union";
335 for(union_typet::componentst::const_iterator
351 else if(src.
id()==ID_incomplete_union)
353 std::string dest=q+
"union";
355 const std::string &tag=src.
get_string(ID_tag);
362 else if(src.
id()==ID_c_enum)
386 for(c_enum_typet::memberst::const_iterator
391 if(it!=members.begin())
404 else if(src.
id()==ID_incomplete_c_enum)
410 std::string result=q+
"enum";
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=
"*";
435 (!declarator.empty() || subtype_followed.
id()==ID_pointer))
436 new_declarator+=
" "+q;
438 new_declarator+=declarator;
441 if(subtype_followed.
id()==ID_code ||
443 (subtype_followed.
id()==ID_array ||
444 subtype_followed.
id()==ID_incomplete_array)))
445 new_declarator=
"("+new_declarator+
")";
449 else if(src.
id()==ID_array)
453 else if(src.
id()==ID_incomplete_array)
458 src.
subtype(), qualifiers, declarator+
"[]");
460 else if(src.
id()==ID_symbol)
463 const irep_idt &typedef_identifer=symbolic_type.
get(ID_typedef);
467 if(typedef_identifer!=
"")
475 if(followed.
id()==ID_struct)
477 std::string dest=q+
"struct";
484 else if(followed.
id()==ID_union)
486 std::string dest=q+
"union";
494 return convert_rec(followed, new_qualifiers, declarator);
497 else if(src.
id()==ID_struct_tag)
502 std::string dest=q+
"struct";
510 else if(src.
id()==ID_union_tag)
515 std::string dest=q+
"union";
523 else if(src.
id()==ID_code)
529 std::string dest=declarator+
"(";
533 if(parameters.empty())
542 for(code_typet::parameterst::const_iterator
543 it=parameters.begin();
544 it!=parameters.end();
547 if(it!=parameters.begin())
550 if(it->get_identifier().empty())
554 std::string arg_declarator=
580 while(non_ptr_type->
id()==ID_pointer)
583 if(non_ptr_type->
id()==ID_code ||
584 non_ptr_type->
id()==ID_array)
585 dest=
convert_rec(return_type, ret_qualifiers, dest);
587 dest=
convert_rec(return_type, ret_qualifiers,
"")+
" "+dest;
593 if(dest[dest.size()-1]==
' ')
594 dest.resize(dest.size()-1);
599 else if(src.
id()==ID_vector)
610 if(tmp==
"signed char" || tmp==
"char")
612 else if(tmp==
"signed short int")
614 else if(tmp==
"signed int")
616 else if(tmp==
"signed long long int")
618 else if(tmp==
"float")
620 else if(tmp==
"double")
626 dest+=
" __attribute__((vector_size (";
628 dest+=
"*sizeof("+subtype+
"))))";
633 else if(src.
id()==ID_gcc_builtin_va_list)
635 return q+
"__builtin_va_list"+d;
637 else if(src.
id()==ID_constructor ||
638 src.
id()==ID_destructor)
640 return q+
"__attribute__(("+
id2string(src.
id())+
")) void"+d;
661 const std::string &qualifiers_str,
662 const std::string &declarator_str)
679 const std::string &qualifiers,
680 const std::string &declarator,
681 bool inc_struct_body,
682 bool inc_padding_components)
687 assert(inc_struct_body || !inc_padding_components);
691 std::string dest=qualifiers+
"struct";
705 if(component.get_is_padding() && !inc_padding_components)
735 const std::string &declarator_str)
751 const std::string &declarator_str,
752 bool inc_size_if_possible)
755 std::string array_suffix;
757 if(
to_array_type(src).size().is_nil() || !inc_size_if_possible)
765 src.
subtype(), qualifiers, declarator_str+array_suffix);
770 unsigned &precedence)
780 if(to_type.
id()==ID_c_bool &&
784 if(to_type.
id()==ID_bool &&
804 const std::string &symbol1,
805 const std::string &symbol2,
854 const std::string &symbol,
865 std::string dest=symbol+
" { ";
894 for(
size_t i=1; i<src.
operands().size(); i+=2)
896 std::string op1, op2;
902 if(src.
operands()[i].id()==ID_member_name)
905 src.
operands()[i].get(ID_component_name);
920 display_component_name=component_name;
924 op1=
"."+
id2string(display_component_name);
952 std::string dest=
"LET ";
974 std::string op0, op1, op2;
1008 unsigned precedence)
1013 bool condition=
true;
1015 std::string dest=
"cond {\n";
1032 condition=!condition;
1042 const std::string &symbol,
1043 unsigned precedence,
1044 bool full_parentheses)
1066 bool use_parentheses0=
1068 (precedence==p0 && full_parentheses) ||
1069 (precedence==p0 && src.
id()!=op0.
id());
1071 if(use_parentheses0)
1074 if(use_parentheses0)
1081 bool use_parentheses1=
1083 (precedence==p1 && full_parentheses) ||
1084 (precedence==p1 && src.
id()!=op1.
id());
1086 if(use_parentheses1)
1089 if(use_parentheses1)
1097 const std::string &symbol,
1098 unsigned precedence,
1099 bool full_parentheses)
1129 bool use_parentheses=
1131 (precedence==p && full_parentheses) ||
1132 (precedence==p && src.
id()!=it->id());
1146 const std::string &symbol,
1147 unsigned precedence)
1155 std::string dest=symbol;
1169 unsigned precedence)
1177 std::string dest=
"POINTER_OBJECT_HAS_TYPE";
1181 dest+=
convert(static_cast<const typet &>(src.
find(
"object_type")));
1198 std::string dest =
"ALLOCATE";
1201 if(src.
type().
id()==ID_pointer &&
1208 dest += op0 +
", " + op1;
1216 unsigned &precedence)
1226 unsigned &precedence)
1229 to_code(src.
op0()).get_statement()!=ID_block)
1237 unsigned &precedence)
1247 unsigned &precedence)
1254 unsigned &precedence)
1264 const std::string &name,
1265 unsigned precedence)
1267 std::string dest=name;
1288 unsigned precedence)
1295 if(*op0.rbegin()==
';')
1296 op0.resize(op0.size()-1);
1300 if(*op1.rbegin()==
';')
1301 op1.resize(op1.size()-1);
1303 std::string dest=op0;
1312 unsigned precedence)
1316 src.
op1().
id()==ID_constant)
1328 const typet &subtype=
1342 std::string dest=name;
1363 unsigned precedence)
1373 unsigned precedence)
1398 unsigned precedence)
1428 const std::string &symbol,
1429 unsigned precedence)
1450 unsigned precedence)
1473 const exprt &src,
unsigned &precedence)
1478 std::string dest=
"POINTER_ARITHMETIC(";
1510 const exprt &src,
unsigned &precedence)
1515 std::string dest=
"POINTER_DIFFERENCE(";
1548 unsigned precedence;
1553 return "."+src.
get_string(ID_component_name);
1558 unsigned precedence;
1568 unsigned precedence)
1576 if(src.
op0().
id()==ID_dereference &&
1581 if(precedence>p || src.
op0().
op0().
id()==ID_typecast)
1584 if(precedence>p || src.
op0().
op0().
id()==ID_typecast)
1593 if(precedence>p || src.
op0().
id()==ID_typecast)
1596 if(precedence>p || src.
op0().
id()==ID_typecast)
1604 if(full_type.
id()!=ID_struct &&
1605 full_type.
id()!=ID_union)
1613 if(component_name!=
"")
1615 const exprt comp_expr=
1621 if(!comp_expr.
get(ID_pretty_name).
empty())
1634 const exprt comp_expr=
1644 unsigned precedence)
1654 unsigned precedence)
1664 unsigned &precedence)
1675 unsigned &precedence)
1681 src.
op0().
id()==ID_predicate_passive_symbol)
1685 std::unordered_map<irep_idt, irep_idt>::const_iterator entry =
1709 if(src.
id()==ID_next_symbol)
1710 dest=
"NEXT("+dest+
")";
1717 unsigned &precedence)
1720 return "nondet_symbol("+
id2string(
id)+
")";
1725 unsigned &precedence)
1727 const std::string &
id=src.
get_string(ID_identifier);
1728 return "ps("+
id+
")";
1733 unsigned &precedence)
1735 const std::string &
id=src.
get_string(ID_identifier);
1736 return "pns("+
id+
")";
1741 unsigned &precedence)
1743 const std::string &
id=src.
get_string(ID_identifier);
1744 return "pps("+
id+
")";
1749 unsigned &precedence)
1751 const std::string &
id=src.
get_string(ID_identifier);
1757 unsigned &precedence)
1759 return "nondet_bool()";
1764 unsigned &precedence)
1769 std::string result=
"<";
1788 unsigned &precedence)
1795 if(type.
id()==ID_integer ||
1796 type.
id()==ID_natural ||
1797 type.
id()==ID_rational)
1801 else if(type.
id()==ID_c_enum ||
1802 type.
id()==ID_c_enum_tag)
1808 if(c_enum_type.
id()!=ID_c_enum)
1821 for(c_enum_typet::memberst::const_iterator
1826 if(it->get_value()==int_value_string)
1827 return "/*enum*/"+
id2string(it->get_base_name());
1833 else if(type.
id()==ID_rational)
1835 else if(type.
id()==ID_bv)
1840 else if(type.
id()==ID_bool)
1844 else if(type.
id()==ID_unsignedbv ||
1845 type.
id()==ID_signedbv ||
1846 type.
id()==ID_c_bit_field ||
1847 type.
id()==ID_c_bool)
1853 type.
id()==ID_c_bit_field?type.
subtype().
get(ID_C_c_type):
1854 type.
get(ID_C_c_type);
1856 if(type.
id()==ID_c_bool)
1866 else if(int_value==
'\r')
1868 else if(int_value==
'\t')
1870 else if(int_value==
'\'')
1872 else if(int_value==
'\\')
1874 else if(int_value>=
' ' && int_value<126)
1894 if(c_type==ID_unsigned_int)
1896 else if(c_type==ID_unsigned_long_int)
1898 else if(c_type==ID_signed_long_int)
1900 else if(c_type==ID_unsigned_long_long_int)
1902 else if(c_type==ID_signed_long_long_int)
1913 dest=
convert(sizeof_expr)+
" /*"+dest+
"*/ ";
1919 else if(type.
id()==ID_floatbv)
1923 if(dest!=
"" && isdigit(dest[dest.size()-1]))
1925 if(dest.find(
'.')==std::string::npos)
1935 else if(dest.size()==4 &&
1936 (dest[0]==
'+' || dest[0]==
'-'))
1940 else if(dest==
"-inf")
1942 else if(dest==
"+NaN")
1944 else if(dest==
"-NaN")
1948 else if(type.
id()==ID_fixedbv)
1952 if(dest!=
"" && isdigit(dest[dest.size()-1]))
1960 else if(type.
id()==ID_array ||
1961 type.
id()==ID_incomplete_array)
1965 else if(type.
id()==ID_pointer)
1973 dest=
"(("+
convert(type)+
")"+dest+
")";
1975 else if(value==std::string(value.
size(),
'0') &&
1980 dest=
"(("+
convert(type)+
")"+dest+
")";
1988 if(src.
op0().
id()==ID_constant)
1992 if(op_value==
"INVALID" ||
1994 op_value==
"NULL+offset")
2003 else if(type.
id()==ID_string)
2028 unsigned &precedence)
2042 unsigned &precedence,
2043 bool include_padding_components)
2047 if(full_type.
id()!=ID_struct)
2056 if(components.size()!=src.
operands().size())
2059 std::string dest=
"{ ";
2061 exprt::operandst::const_iterator o_it=src.
operands().begin();
2070 if(o_it->type().id()==ID_code)
2073 if(component.get_is_padding() && !include_padding_components)
2091 std::string tmp=
convert(*o_it);
2093 if(last_size+40<dest.size())
2096 last_size=dest.size();
2102 dest+=component.get_string(ID_name);
2116 unsigned &precedence)
2120 if(full_type.
id()!=ID_vector)
2123 std::string dest=
"{ ";
2145 if(last_size+40<dest.size())
2148 last_size=dest.size();
2163 unsigned &precedence)
2165 std::string dest=
"{ ";
2184 unsigned &precedence)
2193 bool all_constant=
true;
2196 if(!it->is_constant())
2199 if(src.
get_bool(ID_C_string_constant) &&
2210 dest.reserve(dest.size()+1+src.
operands().size());
2212 bool last_was_hex=
false;
2220 assert(it->is_constant());
2236 case '\n': dest+=
"\\n";
break;
2237 case '\t': dest+=
"\\t";
break;
2238 case '\v': dest+=
"\\v";
break;
2239 case '\b': dest+=
"\\b";
break;
2240 case '\r': dest+=
"\\r";
break;
2241 case '\f': dest+=
"\\f";
break;
2242 case '\a': dest+=
"\\a";
break;
2243 case '\\': dest+=
"\\\\";
break;
2244 case '"': dest+=
"\\\"";
break;
2247 if(ch>=
' ' && ch!=127 && ch<0xff)
2248 dest+=
static_cast<char>(ch);
2251 std::ostringstream oss;
2252 oss <<
"\\x" << std::hex << ch;
2270 if(it->is_not_nil())
2290 unsigned &precedence)
2292 std::string dest=
"{ ";
2299 std::string tmp1=
convert(*it);
2303 std::string tmp2=
convert(*it);
2305 std::string tmp=
"["+tmp1+
"]="+tmp2;
2324 unsigned &precedence)
2327 if(src.
id()!=ID_compound_literal)
2344 if(src.
id()!=ID_compound_literal)
2352 unsigned &precedence)
2356 unsigned precedence;
2360 std::string dest=
".";
2370 unsigned &precedence)
2400 unsigned &precedence)
2430 unsigned &precedence)
2434 std::string dest=
"overflow(\"";
2461 return std::string(indent,
' ');
2476 if(!src.
operands()[1].operands().empty() ||
2477 !src.
operands()[2].operands().empty() ||
2478 !src.
operands()[3].operands().empty() ||
2479 !src.
operands()[4].operands().empty())
2487 if(it->operands().size()==2)
2502 if(it->operands().size()==2)
2519 if(it->id()==ID_gcc_asm_clobbered_register)
2548 unsigned precedence;
2574 unsigned precedence;
2603 unsigned precedence;
2641 unsigned precedence;
2685 unsigned precedence;
2701 const exprt &op=*it;
2703 if(op.
get(ID_statement)!=ID_block)
2705 unsigned precedence;
2741 unsigned precedence;
2749 const symbolt *symbol=
nullptr;
2760 dest +=
"__declspec(dllexport) ";
2763 if(symbol->
type.
id()==ID_code &&
2785 unsigned precedence;
2798 unsigned precedence;
2838 if(it->get(ID_statement)==ID_label)
2873 std::string expr_str;
2878 unsigned precedence;
2883 if(dest.empty() || *dest.rbegin()!=
';')
2893 static bool comment_done=
false;
2907 if(statement==ID_expression)
2910 if(statement==ID_block)
2913 if(statement==ID_switch)
2916 if(statement==ID_for)
2919 if(statement==ID_while)
2922 if(statement==ID_asm)
2925 if(statement==ID_skip)
2928 if(statement==ID_dowhile)
2931 if(statement==ID_ifthenelse)
2934 if(statement==ID_return)
2937 if(statement==ID_goto)
2940 if(statement==ID_printf)
2943 if(statement==ID_fence)
2946 if(statement==ID_input)
2949 if(statement==ID_output)
2952 if(statement==ID_assume)
2955 if(statement==ID_assert)
2958 if(statement==ID_break)
2961 if(statement==ID_continue)
2964 if(statement==ID_decl)
2967 if(statement==ID_decl_block)
2970 if(statement==ID_dead)
2973 if(statement==ID_assign)
2976 if(statement==ID_init)
2979 if(statement==
"lock")
2982 if(statement==
"unlock")
2985 if(statement==ID_atomic_begin)
2986 return indent_str(indent)+
"__CPROVER_atomic_begin();";
2988 if(statement==ID_atomic_end)
2989 return indent_str(indent)+
"__CPROVER_atomic_end();";
2991 if(statement==ID_function_call)
2994 if(statement==ID_label)
2997 if(statement==ID_switch_case)
3000 if(statement==ID_free)
3003 if(statement==ID_array_set)
3006 if(statement==ID_array_copy)
3009 if(statement==ID_array_replace)
3012 if(statement==
"set_may" ||
3013 statement==
"set_must")
3017 unsigned precedence;
3038 unsigned precedence;
3060 unsigned precedence;
3073 unsigned precedence;
3086 unsigned precedence;
3117 if(it!=arguments.begin())
3132 std::string dest=
indent_str(indent)+
"printf(";
3154 std::string dest=
indent_str(indent)+
"FENCE(";
3157 { ID_WRfence, ID_RRfence, ID_RWfence, ID_WWfence,
3158 ID_RRcumul, ID_RWcumul, ID_WWcumul, ID_WRcumul,
3163 for(
unsigned i=0; !att[i].
empty(); i++)
3184 std::string dest=
indent_str(indent)+
"INPUT(";
3206 std::string dest=
indent_str(indent)+
"OUTPUT(";
3227 std::string dest=
indent_str(indent)+
"ARRAY_SET(";
3249 std::string dest=
indent_str(indent)+
"ARRAY_COPY(";
3271 std::string dest=
indent_str(indent)+
"ARRAY_REPLACE(";
3294 unsigned precedence;
3307 unsigned precedence;
3318 std::string labels_string;
3322 labels_string+=
"\n";
3325 labels_string+=
":\n";
3329 return labels_string+tmp;
3336 std::string labels_string;
3340 labels_string+=
"\n";
3342 labels_string+=
"default:\n";
3346 labels_string+=
"\n";
3348 labels_string+=
"case ";
3350 labels_string+=
":\n";
3353 unsigned next_indent=indent;
3359 return labels_string+tmp;
3369 unsigned precedence;
3377 static_cast<const codet &
>(src.
find(ID_code));
3379 std::string dest=
"\n";
3384 std::string assumption_str=
convert(assumption);
3386 dest+=assumption_str;
3399 std::string assertion_str=
convert(assertion);
3401 dest+=assertion_str;
3412 unsigned precedence)
3427 unsigned precedence)
3444 unsigned &precedence)
3449 std::string dest=
"sizeof(";
3450 dest+=
convert(static_cast<const typet&>(src.
find(ID_type_arg)));
3458 unsigned &precedence)
3462 if(src.
id()==ID_plus)
3465 else if(src.
id()==ID_minus)
3468 else if(src.
id()==ID_unary_minus)
3471 else if(src.
id()==ID_unary_plus)
3474 else if(src.
id()==ID_floatbv_plus)
3477 else if(src.
id()==ID_floatbv_minus)
3480 else if(src.
id()==ID_floatbv_mult)
3483 else if(src.
id()==ID_floatbv_div)
3486 else if(src.
id()==ID_floatbv_rem)
3489 else if(src.
id()==ID_floatbv_typecast)
3492 std::string dest=
"FLOAT_TYPECAST(";
3521 else if(src.
id()==ID_sign)
3530 else if(src.
id()==ID_popcount)
3538 else if(src.
id()==ID_invalid_pointer)
3541 else if(src.
id()==ID_good_pointer)
3544 else if(src.
id()==ID_object_size)
3547 else if(src.
id()==
"pointer_arithmetic")
3550 else if(src.
id()==
"pointer_difference")
3553 else if(src.
id() == ID_null_object)
3554 return "NULL-object";
3556 else if(src.
id()==ID_integer_address ||
3557 src.
id()==ID_integer_address_object ||
3558 src.
id()==ID_stack_object ||
3559 src.
id()==ID_static_object)
3564 else if(src.
id()==ID_infinity)
3567 else if(src.
id()==
"builtin-function")
3570 else if(src.
id()==ID_pointer_object)
3573 else if(src.
id()==
"get_must")
3576 else if(src.
id()==
"get_may")
3579 else if(src.
id()==
"object_value")
3582 else if(src.
id()==
"pointer_object_has_type")
3585 else if(src.
id()==ID_array_of)
3588 else if(src.
id()==ID_pointer_offset)
3591 else if(src.
id()==
"pointer_base")
3594 else if(src.
id()==
"pointer_cons")
3597 else if(src.
id()==ID_invalid_pointer)
3600 else if(src.
id()==ID_dynamic_object)
3603 else if(src.
id()==
"is_zero_string")
3606 else if(src.
id()==
"zero_string")
3609 else if(src.
id()==
"zero_string_length")
3612 else if(src.
id()==
"buffer_size")
3615 else if(src.
id()==ID_isnan)
3618 else if(src.
id()==ID_isfinite)
3621 else if(src.
id()==ID_isinf)
3624 else if(src.
id()==ID_bswap)
3631 else if(src.
id()==ID_isnormal)
3634 else if(src.
id()==ID_builtin_offsetof)
3637 else if(src.
id()==ID_gcc_builtin_va_arg)
3640 else if(src.
id()==ID_alignof)
3650 else if(src.
id()==ID_address_of)
3654 else if(src.
op0().
id()==ID_label)
3656 else if(src.
op0().
id()==ID_index &&
3665 else if(src.
id()==ID_dereference)
3669 else if(src.
type().
id()==ID_code)
3671 else if(src.
op0().
id()==ID_plus &&
3682 else if(src.
id()==ID_index)
3685 else if(src.
id()==ID_member)
3688 else if(src.
id()==
"array-member-value")
3691 else if(src.
id()==
"struct-member-value")
3694 else if(src.
id()==ID_function_application)
3699 else if(src.
id()==ID_side_effect)
3702 if(statement==ID_preincrement)
3704 else if(statement==ID_predecrement)
3706 else if(statement==ID_postincrement)
3708 else if(statement==ID_postdecrement)
3710 else if(statement==ID_assign_plus)
3712 else if(statement==ID_assign_minus)
3714 else if(statement==ID_assign_mult)
3716 else if(statement==ID_assign_div)
3718 else if(statement==ID_assign_mod)
3720 else if(statement==ID_assign_shl)
3722 else if(statement==ID_assign_shr)
3724 else if(statement==ID_assign_bitand)
3726 else if(statement==ID_assign_bitxor)
3728 else if(statement==ID_assign_bitor)
3730 else if(statement==ID_assign)
3732 else if(statement==ID_function_call)
3736 else if(statement == ID_allocate)
3738 else if(statement==ID_printf)
3740 else if(statement==ID_nondet)
3742 else if(statement==
"prob_coin")
3744 else if(statement==
"prob_unif")
3746 else if(statement==ID_statement_expression)
3748 else if(statement==ID_gcc_builtin_va_arg_next)
3754 else if(src.
id()==ID_literal)
3757 else if(src.
id()==ID_not)
3760 else if(src.
id()==ID_bitnot)
3763 else if(src.
id()==ID_mult)
3766 else if(src.
id()==ID_div)
3769 else if(src.
id()==ID_mod)
3772 else if(src.
id()==ID_shl)
3775 else if(src.
id()==ID_ashr || src.
id()==ID_lshr)
3778 else if(src.
id()==ID_lt || src.
id()==ID_gt ||
3779 src.
id()==ID_le || src.
id()==ID_ge)
3782 else if(src.
id()==ID_notequal)
3785 else if(src.
id()==ID_equal)
3788 else if(src.
id()==ID_ieee_float_equal)
3791 else if(src.
id()==ID_width)
3794 else if(src.
id()==ID_concatenation)
3797 else if(src.
id()==ID_ieee_float_notequal)
3800 else if(src.
id()==ID_abs)
3803 else if(src.
id()==ID_complex_real)
3806 else if(src.
id()==ID_complex_imag)
3809 else if(src.
id()==ID_complex)
3812 else if(src.
id()==ID_bitand)
3815 else if(src.
id()==ID_bitxor)
3818 else if(src.
id()==ID_bitor)
3821 else if(src.
id()==ID_and)
3824 else if(src.
id()==ID_or)
3827 else if(src.
id()==ID_xor)
3830 else if(src.
id()==ID_implies)
3833 else if(src.
id()==ID_if)
3836 else if(src.
id()==ID_forall)
3839 else if(src.
id()==ID_exists)
3842 else if(src.
id()==ID_lambda)
3845 else if(src.
id()==ID_with)
3848 else if(src.
id()==ID_update)
3851 else if(src.
id()==ID_member_designator)
3854 else if(src.
id()==ID_index_designator)
3857 else if(src.
id()==ID_symbol)
3860 else if(src.
id()==ID_next_symbol)
3863 else if(src.
id()==ID_nondet_symbol)
3866 else if(src.
id()==ID_predicate_symbol)
3869 else if(src.
id()==ID_predicate_next_symbol)
3872 else if(src.
id()==ID_predicate_passive_symbol)
3875 else if(src.
id()==
"quant_symbol")
3878 else if(src.
id()==ID_nondet_bool)
3881 else if(src.
id()==ID_object_descriptor)
3884 else if(src.
id()==
"Hoare")
3887 else if(src.
id()==ID_code)
3890 else if(src.
id()==ID_constant)
3893 else if(src.
id()==ID_string_constant)
3896 else if(src.
id()==ID_struct)
3899 else if(src.
id()==ID_vector)
3902 else if(src.
id()==ID_union)
3905 else if(src.
id()==ID_array)
3908 else if(src.
id() == ID_array_list)
3911 else if(src.
id()==ID_typecast)
3914 else if(src.
id()==ID_comma)
3917 else if(src.
id()==ID_ptr_object)
3918 return "PTR_OBJECT("+
id2string(src.
get(ID_identifier))+
")";
3920 else if(src.
id()==ID_cond)
3923 else if(src.
id()==ID_overflow_unary_minus ||
3924 src.
id()==ID_overflow_minus ||
3925 src.
id()==ID_overflow_mult ||
3926 src.
id()==ID_overflow_plus)
3929 else if(src.
id()==ID_unknown)
3932 else if(src.
id()==ID_invalid)
3935 else if(src.
id()==ID_extractbit)
3938 else if(src.
id()==ID_extractbits)
3941 else if(src.
id()==ID_initializer_list ||
3942 src.
id()==ID_compound_literal)
3945 else if(src.
id()==ID_designated_initializer)
3948 else if(src.
id()==ID_sizeof)
3951 else if(src.
id()==ID_let)
3954 else if(src.
id()==ID_type)
3963 unsigned precedence;
3971 expr2c.get_shorthands(expr);
3972 return expr2c.convert(expr);
3979 return expr2c.convert(type);
std::string convert_statement_expression(const exprt &src, unsigned &precendence)
const irep_idt & get_statement() const
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
The type of an expression.
std::string convert_code_assume(const codet &src, unsigned indent)
const codet & then_case() const
bool is_signed(const typet &t)
Convenience function – is the type signed?
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
struct configt::ansi_ct ansi_c
std::string convert_complex(const exprt &src, unsigned precedence)
std::string to_ansi_c_string() const
const std::string & id2string(const irep_idt &d)
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.
void get_shorthands(const exprt &expr)
application of (mathematical) function
std::string convert_code_expression(const codet &src, unsigned indent)
std::string convert_multi_ary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
const exprt & cond() const
std::string convert_code_continue(const codet &src, unsigned indent)
std::string convert_code_fence(const codet &src, unsigned indent)
const exprt & cond() const
std::string expr2string() const
mp_integer::ullong_t integer2ulong(const mp_integer &n)
std::string convert_Hoare(const exprt &src)
const codet & body() const
bool has_ellipsis() const
const codet & body() const
std::string convert_union(const exprt &src, unsigned &precedence)
unsignedbv_typet unsigned_int_type()
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
std::string convert_unary_post(const exprt &src, const std::string &symbol, unsigned precedence)
const irep_idt & get_function() const
#define forall_expr(it, expr)
std::vector< componentt > componentst
std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent)
const irep_idt & get_value() const
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
std::vector< parametert > parameterst
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
std::string convert_overflow(const exprt &src, unsigned &precedence)
exprt build_sizeof_expr(const constant_exprt &expr, const namespacet &ns)
const componentst & components() const
std::string convert_code_block(const code_blockt &src, unsigned indent)
std::string convert_code(const codet &src)
std::size_t get_component_number() const
const memberst & members() const
std::string convert_array_of(const exprt &src, unsigned precedence)
bitvector_typet double_type()
std::string convert_code_unlock(const codet &src, unsigned indent)
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
unsignedbv_typet size_type()
const irep_idt & get_flavor() const
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual std::string convert_symbol(const exprt &src, unsigned &precedence)
A constant literal expression.
std::string convert_code_break(const codet &src, unsigned indent)
std::string convert_code_decl(const codet &src, unsigned indent)
bool get_bool(const irep_namet &name) const
std::string convert_code_return(const codet &src, unsigned indent)
const typet & follow_tag(const union_tag_typet &) const
std::string convert_predicate_next_symbol(const exprt &src, unsigned &precedence)
virtual std::string convert(const typet &src)
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
std::string convert_nondet_symbol(const nondet_symbol_exprt &, unsigned &precedence)
irep_idt id_shorthand(const irep_idt &identifier) const
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
std::string convert_sizeof(const exprt &src, unsigned &precedence)
std::string convert_code_printf(const codet &src, unsigned indent)
const exprt & case_op() const
Extract member of struct or union.
std::string convert_binary(const exprt &src, const std::string &symbol, unsigned precedence, bool full_parentheses)
std::string convert_predicate_passive_symbol(const exprt &src, unsigned &precedence)
std::string convert_code_free(const codet &src, unsigned indent)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
std::string convert_unary(const exprt &src, const std::string &symbol, unsigned precedence)
const code_assignt & to_code_assign(const codet &code)
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
const irep_idt & id() const
std::string convert_literal(const exprt &src, unsigned &precedence)
std::size_t long_long_int_width
std::string convert_code_assign(const code_assignt &src, unsigned indent)
std::string convert_code_label(const code_labelt &src, unsigned indent)
std::string convert_byte_update(const exprt &src, unsigned precedence)
A reference into the symbol table.
std::string convert_pointer_object_has_type(const exprt &src, unsigned precedence)
std::string convert_nondet_bool(const exprt &src, unsigned &precedence)
bitvector_typet float_type()
std::string convert_code_input(const codet &src, unsigned indent)
const irep_idt & get_identifier() const
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > ns_collision
virtual std::unique_ptr< qualifierst > clone() const =0
std::string convert_prob_coin(const exprt &src, unsigned &precedence)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
std::size_t get_fraction_bits() const
std::string convert_index_designator(const exprt &src)
const code_dowhilet & to_code_dowhile(const codet &code)
A constant-size array type.
const code_whilet & to_code_while(const codet &code)
std::string convert_code_array_set(const codet &src, unsigned indent)
std::string convert_member(const member_exprt &src, unsigned precedence)
std::string convert_pointer_difference(const exprt &src, unsigned &precedence)
std::string convert_trinary(const exprt &src, const std::string &symbol1, const std::string &symbol2, unsigned precedence)
std::string convert_code_asm(const code_asmt &src, unsigned indent)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
const irep_idt & get(const irep_namet &name) const
const exprt & size() const
virtual void read(const typet &src) override
std::string convert_initializer_list(const exprt &src, unsigned &precedence)
std::string convert_code_dead(const codet &src, unsigned indent)
A label for branch targets.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const code_returnt & to_code_return(const codet &code)
std::string convert_code_lock(const codet &src, unsigned indent)
std::string type2c(const typet &type, const namespacet &ns)
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Base class for tree-like data structures with sharing.
#define forall_operands(it, expr)
std::string convert_array_list(const exprt &src, unsigned &precedence)
std::string convert_with(const exprt &src, unsigned precedence)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
std::string convert_prob_uniform(const exprt &src, unsigned &precedence)
const code_switch_caset & to_code_switch_case(const codet &code)
const typet & follow(const typet &) const
void irep2lisp(const irept &src, lispexprt &dest)
std::unordered_map< irep_idt, irep_idt > shorthands
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
std::string convert_extractbits(const exprt &src, unsigned precedence)
virtual std::string as_string() const override
std::string convert_extractbit(const exprt &src, unsigned precedence)
std::string convert_side_effect_expr_function_call(const side_effect_expr_function_callt &src, unsigned &precedence)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
bool has_operands() const
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::size_t get_width() const
std::string convert_vector(const exprt &src, unsigned &precedence)
std::string c_type_as_string(const irep_idt &c_type)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
const irep_idt & get_pretty_name() const
symbol_exprt & function()
std::vector< exprt > operandst
std::string convert_predicate_symbol(const exprt &src, unsigned &precedence)
std::string convert_nondet(const exprt &src, unsigned &precedence)
bitvector_typet long_double_type()
std::string convert_norep(const exprt &src, unsigned &precedence)
std::string convert_code_assert(const codet &src, unsigned indent)
std::string convert_index(const exprt &src, unsigned precedence)
unsigned integer2unsigned(const mp_integer &n)
std::string convert_array_member_value(const exprt &src, unsigned precedence)
A function call side effect.
std::string convert_byte_extract(const exprt &src, unsigned precedence)
std::string convert_member_designator(const exprt &src)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
bitvector_typet wchar_t_type()
std::string convert_code_dowhile(const code_dowhilet &src, unsigned indent)
Expression to hold a nondeterministic choice.
Base type of C structs and unions, and C++ classes.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
std::string convert_quantified_symbol(const exprt &src, unsigned &precedence)
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
std::string convert_code_array_copy(const codet &src, unsigned indent)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
std::string convert_update(const exprt &src, unsigned precedence)
std::string convert_cond(const exprt &src, unsigned precedence)
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
std::string convert_code_for(const code_fort &src, unsigned indent)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
A ‘do while’ instruction.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
const source_locationt & source_location() const
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
An inline assembler statement.
irep_idt get_component_name() const
std::string convert_code_decl_block(const codet &src, unsigned indent)
std::string convert_code_array_replace(const codet &src, unsigned indent)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
std::string convert_pointer_arithmetic(const exprt &src, unsigned &precedence)
std::string expr2c(const exprt &expr, const namespacet &ns)
const std::string & get_string(const irep_namet &name) const
exprt::operandst & arguments()
const std::string & id_string() const
std::string convert_struct_member_value(const exprt &src, unsigned precedence)
const codet & to_code(const exprt &expr)
std::string convert_array(const exprt &src, unsigned &precedence)
const irep_idt & get_label() const
std::string convert_allocate(const exprt &src, unsigned &precedence)
const code_fort & to_code_for(const codet &code)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Expression to hold a symbol (variable)
std::string convert_designated_initializer(const exprt &src, unsigned &precedence)
const char * c_str() const
const code_blockt & to_code_block(const codet &code)
bool has_suffix(const std::string &s, const std::string &suffix)
std::string MetaString(const std::string &in)
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
std::string convert_code_goto(const codet &src, unsigned indent)
A statement in a programming language.
std::unordered_set< irep_idt > find_symbols_sett
signedbv_typet signed_int_type()
const irep_idt & get_comment() const
const code_labelt & to_code_label(const codet &code)
std::string convert_comma(const exprt &src, unsigned precedence)
const typet & subtype() const
std::string convert_code_while(const code_whilet &src, unsigned indent)
std::string convert_code_output(const codet &src, unsigned indent)
std::string convert_object_descriptor(const exprt &src, unsigned &precedence)
std::string to_ansi_c_string() const
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast a generic exprt to a nondet_symbol_exprt.
static std::string clean_identifier(const irep_idt &id)
std::size_t long_int_width
std::string convert_code_init(const codet &src, unsigned indent)
const exprt & cond() const
const codet & else_case() const
const code_ifthenelset & to_code_ifthenelse(const codet &code)
std::vector< c_enum_membert > memberst
std::string convert_quantifier(const exprt &src, const std::string &symbol, unsigned precedence)
std::string convert_let(const let_exprt &, unsigned precedence)
const codet & body() const
virtual std::string convert_constant_bool(bool boolean_value)
To get the C-like representation of a given boolean value.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irept & find(const irep_namet &name) const
void find_symbols(const exprt &src, find_symbols_sett &dest)
code_asmt & to_code_asm(codet &code)
bitvector_typet char_type()
const typet & return_type() const
std::string convert_code_switch(const codet &src, unsigned indent)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
std::string convert_typecast(const typecast_exprt &src, unsigned &precedence)
std::size_t short_int_width
static std::string indent_str(unsigned indent)
std::string convert_function_application(const function_application_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::size_t long_double_width
const componentt & get_component(const irep_idt &component_name) const
const code_function_callt & to_code_function_call(const codet &code)
std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent)