{

const symbolt *symbol;

if(!ns.lookup(identifier, symbol) &&

!symbol->base_name.empty() &&

has_suffix(id2string(identifier), id2string(symbol->base_name)))

return symbol->base_name;

std::string sh=id2string(identifier);

std::string::size_type pos=sh.rfind("::");

if(pos!=std::string::npos)

sh.erase(0, pos+2);

return sh;

{

std::string dest=id2string(id);

std::string::size_type c_pos=dest.find("::");

if(c_pos!=std::string::npos &&

dest.rfind("::")==c_pos)

dest.erase(0, c_pos+2);

else if(c_pos!=std::string::npos)

{

for(char &ch : dest)

if(ch == ':')

ch = '$';

else if(ch == '-')

ch = '_';

}

// rewrite . as used in ELF section names

std::replace(dest.begin(), dest.end(), '.', '_');

return dest;

{

const std::unordered_set<irep_idt> symbols = find_symbol_identifiers(expr);

// avoid renaming parameters, if possible

for(const auto &symbol_id : symbols)

{

const symbolt *symbol;

bool is_param = !ns.lookup(symbol_id, symbol) && symbol->is_parameter;

if(!is_param)

continue;

irep_idt sh = id_shorthand(symbol_id);

std::string func = id2string(symbol_id);

func = func.substr(0, func.rfind("::"));

// if there is a global symbol of the same name as the shorthand (even if

// not present in this particular expression) then there is a collision

const symbolt *global_symbol;

if(!ns.lookup(sh, global_symbol))

sh = func + "$$" + id2string(sh);

ns_collision[func].insert(sh);

if(!shorthands.insert(std::make_pair(symbol_id, sh)).second)

UNREACHABLE;

}

for(const auto &symbol_id : symbols)

{

if(shorthands.find(symbol_id) != shorthands.end())

continue;

irep_idt sh = id_shorthand(symbol_id);

bool has_collision=

ns_collision[irep_idt()].find(sh)!=

ns_collision[irep_idt()].end();

if(!has_collision)

{

// if there is a global symbol of the same name as the shorthand (even if

// not present in this particular expression) then there is a collision

const symbolt *symbol;

has_collision=!ns.lookup(sh, symbol);

}

if(!has_collision)

{

irep_idt func;

const symbolt *symbol;

// we use the source-level function name as a means to detect collisions,

// which is ok, because this is about generating user-visible output

if(!ns.lookup(symbol_id, symbol))

func=symbol->location.get_function();

has_collision=!ns_collision[func].insert(sh).second;

}

if(!has_collision)

{

// We could also conflict with a function argument, the code below

// finds the function we're in, and checks we don't conflict with

// any argument to the function

const std::string symbol_str = id2string(symbol_id);

const std::string func = symbol_str.substr(0, symbol_str.find("::"));

const symbolt *func_symbol;

if(!ns.lookup(func, func_symbol))

{

if(can_cast_type<code_typet>(func_symbol->type))

{

const auto func_type =

type_checked_cast<code_typet>(func_symbol->type);

const auto params = func_type.parameters();

for(const auto &param : params)

{

const auto param_id = param.get_identifier();

if(param_id != symbol_id && sh == id_shorthand(param_id))

{

has_collision = true;

break;

}

}

}

}

}

if(has_collision)

sh = clean_identifier(symbol_id);

shorthands.insert(std::make_pair(symbol_id, sh));

}

const typet &src,

const c_qualifierst &qualifiers,

const std::string &declarator)

{

std::unique_ptr<c_qualifierst> clone = qualifiers.clone();

c_qualifierst &new_qualifiers = *clone;

new_qualifiers.read(src);

std::string q=new_qualifiers.as_string();

std::string d = declarator.empty() ? declarator : " " + declarator;

if(!configuration.expand_typedef && src.find(ID_C_typedef).is_not_nil())

{

return q+id2string(src.get(ID_C_typedef))+d;

}

if(src.id()==ID_bool)

{

return q + CPROVER_PREFIX + "bool" + d;

}

else if(src.id()==ID_c_bool)

{

return q+"_Bool"+d;

}

else if(src.id()==ID_string)

{

return q + CPROVER_PREFIX + "string" + d;

}

else if(

src.id() == ID_natural || src.id() == ID_integer ||

src.id() == ID_rational || src.id() == ID_real)

{

return q + CPROVER_PREFIX + src.id_string() + d;

}

else if(src.id()==ID_empty)

{

return q+"void"+d;

}

else if(src.id()==ID_complex)

{

// these take more or less arbitrary subtypes

return q + "_Complex " + convert(to_complex_type(src).subtype()) + d;

}

else if(src.id()==ID_floatbv)

{

std::size_t width=to_floatbv_type(src).get_width();

if(width==config.ansi_c.single_width)

return q+"float"+d;

else if(width==config.ansi_c.double_width)

return q+"double"+d;

else if(width==config.ansi_c.long_double_width)

return q+"long double"+d;

else

{

std::string swidth = std::to_string(width);

std::string fwidth=src.get_string(ID_f);

return q + CPROVER_PREFIX + "floatbv[" + swidth + "][" + fwidth + "]";

}

}

else if(src.id()==ID_fixedbv)

{

const std::size_t width=to_fixedbv_type(src).get_width();

const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits();

return q + CPROVER_PREFIX + "fixedbv[" + std::to_string(width) + "][" +

std::to_string(fraction_bits) + "]" + d;

}

else if(src.id()==ID_c_bit_field)

{

std::string width=std::to_string(to_c_bit_field_type(src).get_width());

return q + convert(to_c_bit_field_type(src).underlying_type()) + d + " : " +

width;

}

else if(src.id()==ID_signedbv ||

src.id()==ID_unsignedbv)

{

// annotated?

irep_idt c_type=src.get(ID_C_c_type);

const std::string c_type_str=c_type_as_string(c_type);

if(c_type==ID_char &&

config.ansi_c.char_is_unsigned!=(src.id()==ID_unsignedbv))

{

if(src.id()==ID_signedbv)

return q+"signed char"+d;

else

return q+"unsigned char"+d;

}

else if(c_type!=ID_wchar_t && !c_type_str.empty())

return q+c_type_str+d;

// There is also wchar_t among the above, but this isn't a C type.

const std::size_t width = to_bitvector_type(src).get_width();

bool is_signed=src.id()==ID_signedbv;

std::string sign_str=is_signed?"signed ":"unsigned ";

if(width==config.ansi_c.int_width)

{

if(is_signed)

sign_str.clear();

return q+sign_str+"int"+d;

}

else if(width==config.ansi_c.long_int_width)

{

if(is_signed)

sign_str.clear();

return q+sign_str+"long int"+d;

}

else if(width==config.ansi_c.char_width)

{

// always include sign

return q+sign_str+"char"+d;

}

else if(width==config.ansi_c.short_int_width)

{

if(is_signed)

sign_str.clear();

return q+sign_str+"short int"+d;

}

else if(width==config.ansi_c.long_long_int_width)

{

if(is_signed)

sign_str.clear();

return q+sign_str+"long long int"+d;

}

else if(width==128)

{

if(is_signed)

sign_str.clear();

return q + sign_str + "__int128" + d;

}

else

{

return q + sign_str + CPROVER_PREFIX + "bitvector[" +

integer2string(width) + "]" + d;

}

}

else if(src.id()==ID_struct)

{

return convert_struct_type(src, q, d);

}

else if(src.id()==ID_union)

{

const union_typet &union_type=to_union_type(src);

std::string dest=q+"union";

const irep_idt &tag=union_type.get_tag();

if(!tag.empty())

dest+=" "+id2string(tag);

if(!union_type.is_incomplete())

{

dest += " {";

for(const auto &c : union_type.components())

{

dest += ' ';

dest += convert_with_identifier(c.type(), id2string(c.get_name()));

dest += ';';

}

dest += " }";

}

dest+=d;

return dest;

}

else if(src.id()==ID_c_enum)

{

std::string result;

result+=q;

result+="enum";

// do we have a tag?

const irept &tag=src.find(ID_tag);

if(tag.is_nil())

{

}

else

{

result+=' ';

result+=tag.get_string(ID_C_base_name);

}

result+=' ';

if(!to_c_enum_type(src).is_incomplete())

{

const c_enum_typet &c_enum_type = to_c_enum_type(src);

const bool is_signed = c_enum_type.underlying_type().id() == ID_signedbv;

const auto width =

to_bitvector_type(c_enum_type.underlying_type()).get_width();

result += '{';

// add members

const c_enum_typet::memberst &members = c_enum_type.members();

for(c_enum_typet::memberst::const_iterator it = members.begin();

it != members.end();

it++)

{

mp_integer int_value = bvrep2integer(it->get_value(), width, is_signed);

if(it != members.begin())

result += ',';

result += ' ';

result += id2string(it->get_base_name());

result += '=';

result += integer2string(int_value);

}

result += " }";

}

result += d;

return result;

}

else if(src.id()==ID_c_enum_tag)

{

const c_enum_tag_typet &c_enum_tag_type=to_c_enum_tag_type(src);

const symbolt &symbol=ns.lookup(c_enum_tag_type);

std::string result=q+"enum";

result+=" "+id2string(symbol.base_name);

result+=d;

return result;

}

else if(src.id()==ID_pointer)

{

c_qualifierst sub_qualifiers;

const typet &base_type = to_pointer_type(src).base_type();

sub_qualifiers.read(base_type);

// The star gets attached to the declarator.

std::string new_declarator="*";

if(!q.empty() && (!declarator.empty() || base_type.id() == ID_pointer))

{

new_declarator+=" "+q;

}

new_declarator+=declarator;

// Depending on precedences, we may add parentheses.

if(

base_type.id() == ID_code ||

(sizeof_nesting == 0 && base_type.id() == ID_array))

{

new_declarator="("+new_declarator+")";

}

return convert_rec(base_type, sub_qualifiers, new_declarator);

}

else if(src.id()==ID_array)

{

return convert_array_type(src, qualifiers, declarator);

}

else if(src.id()==ID_struct_tag)

{

const struct_tag_typet &struct_tag_type=

to_struct_tag_type(src);

std::string dest=q+"struct";

const std::string &tag=ns.follow_tag(struct_tag_type).get_string(ID_tag);

if(!tag.empty())

dest+=" "+tag;

dest+=d;

return dest;

}

else if(src.id()==ID_union_tag)

{

const union_tag_typet &union_tag_type=

to_union_tag_type(src);

std::string dest=q+"union";

const std::string &tag=ns.follow_tag(union_tag_type).get_string(ID_tag);

if(!tag.empty())

dest+=" "+tag;

dest+=d;

return dest;

}

else if(src.id()==ID_code)

{

const code_typet &code_type=to_code_type(src);

// C doesn't really have syntax for function types,

// i.e., the following won't parse without declarator

std::string dest=declarator+"(";

const code_typet::parameterst &parameters=code_type.parameters();

if(parameters.empty())

{

if(!code_type.has_ellipsis())

dest+="void"; // means 'no parameters'

}

else

{

for(code_typet::parameterst::const_iterator

it=parameters.begin();

it!=parameters.end();

it++)

{

if(it!=parameters.begin())

dest+=", ";

if(it->get_identifier().empty())

dest+=convert(it->type());

else

{

std::string arg_declarator=

convert(symbol_exprt(it->get_identifier(), it->type()));

dest += convert_with_identifier(it->type(), arg_declarator);

}

}

if(code_type.has_ellipsis())

dest+=", ...";

}

dest+=')';

c_qualifierst ret_qualifiers;

ret_qualifiers.read(code_type.return_type());

// _Noreturn should go with the return type

if(new_qualifiers.is_noreturn)

{

ret_qualifiers.is_noreturn=true;

new_qualifiers.is_noreturn=false;

q=new_qualifiers.as_string();

}

const typet &return_type=code_type.return_type();

// return type may be a function pointer or array

const typet *non_ptr_type = &return_type;

while(non_ptr_type->id()==ID_pointer)

non_ptr_type = &(to_pointer_type(*non_ptr_type).base_type());

if(non_ptr_type->id()==ID_code ||

non_ptr_type->id()==ID_array)

dest=convert_rec(return_type, ret_qualifiers, dest);

else

dest=convert_rec(return_type, ret_qualifiers, "")+" "+dest;

if(!q.empty())

{

dest+=" "+q;

// strip trailing space off q

if(dest[dest.size()-1]==' ')

dest.resize(dest.size()-1);

}

return dest;

}

else if(src.id()==ID_vector)

{

const vector_typet &vector_type=to_vector_type(src);

const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.size());

std::string dest="__gcc_v"+integer2string(size_int);

std::string tmp = convert(vector_type.element_type());

if(tmp=="signed char" || tmp=="char")

dest+="qi";

else if(tmp=="signed short int")

dest+="hi";

else if(tmp=="signed int")

dest+="si";

else if(tmp=="signed long long int")

dest+="di";

else if(tmp=="float")

dest+="sf";

else if(tmp=="double")

dest+="df";

else

{

const std::string subtype = convert(vector_type.element_type());

dest=subtype;

dest+=" __attribute__((vector_size (";

dest+=convert(vector_type.size());

dest+="*sizeof("+subtype+"))))";

}

return q+dest+d;

}

else if(src.id()==ID_constructor ||

src.id()==ID_destructor)

{

return q+"__attribute__(("+id2string(src.id())+")) void"+d;

}

else if(src.id() == ID_bv)

{

// annotated?

irep_idt c_type = src.get(ID_C_c_type);

if(c_type == ID_c_signed_bitint)

{

return "_BitInt(" + src.get_string(ID_C_c_bitint_width) + ")";

}

else if(c_type == ID_c_unsigned_bitint)

{

return "unsigned _BitInt(" + src.get_string(ID_C_c_bitint_width) + ")";

}

}

{

lispexprt lisp;

irep2lisp(src, lisp);

std::string dest="irep(\""+MetaString(lisp.expr2string())+"\")";

dest+=d;

return dest;

}

const typet &src,

const std::string &qualifiers_str,

const std::string &declarator_str)

{

return convert_struct_type(

src,

qualifiers_str,

declarator_str,

configuration.print_struct_body_in_type,

configuration.include_struct_padding_components);

const typet &src,

const std::string &qualifiers,

const std::string &declarator,

bool inc_struct_body,

bool inc_padding_components)

{

// Either we are including the body (in which case it makes sense to include

// or exclude the parameters) or there is no body so therefore we definitely

// shouldn't be including the parameters

INVARIANT(

inc_struct_body || !inc_padding_components, "inconsistent configuration");

const struct_typet &struct_type=to_struct_type(src);

std::string dest=qualifiers+"struct";

const irep_idt &tag=struct_type.get_tag();

if(!tag.empty())

dest+=" "+id2string(tag);

if(inc_struct_body && !struct_type.is_incomplete())

{

dest+=" {";

for(const auto &component : struct_type.components())

{

// Skip padding parameters unless we including them

if(component.get_is_padding() && !inc_padding_components)

{

continue;

}

dest+=' ';

dest += convert_with_identifier(

component.type(), id2string(component.get_name()));

dest+=';';

}

dest+=" }";

}

dest+=declarator;

return dest;

const typet &src,

const c_qualifierst &qualifiers,

const std::string &declarator_str)

{

return convert_array_type(

src, qualifiers, declarator_str, configuration.include_array_size);

const typet &src,

const c_qualifierst &qualifiers,

const std::string &declarator_str,

bool inc_size_if_possible)

{

// The [...] gets attached to the declarator.

std::string array_suffix;

if(to_array_type(src).size().is_nil() || !inc_size_if_possible)

array_suffix="[]";

else

array_suffix="["+convert(to_array_type(src).size())+"]";

// This won't really parse without declarator.

// Note that qualifiers are passed down.

return convert_rec(

to_array_type(src).element_type(),

qualifiers,

declarator_str + array_suffix);

const typecast_exprt &src,

unsigned &precedence)

{

if(src.operands().size()!=1)

return convert_norep(src, precedence);

// some special cases

const typet &to_type = src.type();

const typet &from_type = src.op().type();

if(to_type.id()==ID_c_bool &&

from_type.id()==ID_bool)

return convert_with_precedence(src.op(), precedence);

if(to_type.id()==ID_bool &&

from_type.id()==ID_c_bool)

return convert_with_precedence(src.op(), precedence);

std::string dest = "(" + convert(to_type) + ")";

unsigned p;

std::string tmp=convert_with_precedence(src.op(), p);

if(precedence>p)

dest+='(';

dest+=tmp;

if(precedence>p)

dest+=')';

return dest;

const ternary_exprt &src,

const std::string &symbol1,

const std::string &symbol2,

unsigned precedence)

{

const exprt &op0=src.op0();

const exprt &op1=src.op1();

const exprt &op2=src.op2();

unsigned p0, p1, p2;

std::string s_op0=convert_with_precedence(op0, p0);

std::string s_op1=convert_with_precedence(op1, p1);

std::string s_op2=convert_with_precedence(op2, p2);

std::string dest;

if(precedence>=p0)

dest+='(';

dest+=s_op0;

if(precedence>=p0)

dest+=')';

dest+=' ';

dest+=symbol1;

dest+=' ';

if(precedence>=p1)

dest+='(';

dest+=s_op1;

if(precedence>=p1)

dest+=')';

dest+=' ';

dest+=symbol2;

dest+=' ';

if(precedence>=p2)

dest+='(';

dest+=s_op2;

if(precedence>=p2)

dest+=')';

return dest;

const binding_exprt &src,

const std::string &symbol,

unsigned precedence)

{

// our made-up syntax can only do one symbol

if(src.variables().size() != 1)

return convert_norep(src, precedence);

unsigned p0, p1;

std::string op0 = convert_with_precedence(src.variables().front(), p0);

std::string op1 = convert_with_precedence(src.where(), p1);

std::string dest=symbol+" { ";

dest += convert(src.variables().front().type());

dest+=" "+op0+"; ";

dest+=op1;

dest+=" }";

return dest;

const exprt &src,

unsigned precedence)

{

if(src.operands().size()<3)

return convert_norep(src, precedence);

unsigned p0;

const auto &old = to_with_expr(src).old();

std::string op0 = convert_with_precedence(old, p0);

std::string dest;

if(precedence>p0)

dest+='(';

dest+=op0;

if(precedence>p0)

dest+=')';

dest+=" WITH [";

for(size_t i=1; i<src.operands().size(); i+=2)

{

std::string op1, op2;

unsigned p1, p2;

if(i!=1)

dest+=", ";

if(src.operands()[i].id()==ID_member_name)

{

const irep_idt &component_name=

src.operands()[i].get(ID_component_name);

const struct_union_typet::componentt &comp_expr =

(old.type().id() == ID_struct_tag || old.type().id() == ID_union_tag)

? ns.follow_tag(to_struct_or_union_tag_type(old.type()))

.get_component(component_name)

: to_struct_union_type(old.type()).get_component(component_name);

CHECK_RETURN(comp_expr.is_not_nil());

irep_idt display_component_name;

if(comp_expr.get_pretty_name().empty())

display_component_name=component_name;

else

display_component_name=comp_expr.get_pretty_name();

op1="."+id2string(display_component_name);

p1=10;

}

else

op1=convert_with_precedence(src.operands()[i], p1);

op2=convert_with_precedence(src.operands()[i+1], p2);

dest+=op1;

dest+=":=";

dest+=op2;

}

dest+=']';

return dest;

const let_exprt &src,

unsigned precedence)

{

std::string dest = "LET ";

bool first = true;

const auto &values = src.values();

auto values_it = values.begin();

for(auto &v : src.variables())

{

if(first)

first = false;

else

dest += ", ";

dest += convert(v) + "=" + convert(*values_it);

++values_it;

}

dest += " IN " + convert(src.where());

return dest;

{

std::string dest;

dest+="UPDATE(";

std::string op0, op1, op2;

unsigned p0, p2;

op0 = convert_with_precedence(src.op0(), p0);

op2 = convert_with_precedence(src.op2(), p2);

if(precedence>p0)

dest+='(';

dest+=op0;

if(precedence>p0)

dest+=')';

dest+=", ";

const exprt &designator = src.op1();

for(const auto &op : designator.operands())

dest += convert(op);

dest+=", ";

if(precedence>p2)

dest+='(';

dest+=op2;

if(precedence>p2)

dest+=')';

dest+=')';

return dest;