48 #include <unordered_set> 64 for(std::size_t i=0; i<what.
size(); i++)
67 else if(
p[i]!=
'?' &&
p[i]!=what[i])
70 return p[what.
size()]==0;
98 for(std::size_t i=0; i<parameters.size(); ++i)
102 if(i==0 && parameters[i].get_this())
108 parameters[i].set_base_name(base_name);
109 parameters[i].set_identifier(identifier);
114 parameter_symbol.
mode=ID_java;
115 parameter_symbol.
name=identifier;
116 parameter_symbol.
type=parameters[i].type();
117 symbol_table.
add(parameter_symbol);
123 return pattern==what;
128 return id2string(method_name).find(
"<init>") != std::string::npos;
135 error() <<
"malformed bytecode (pop too high)" <<
eom;
141 for(std::size_t i=0; i<n; i++)
151 std::size_t residue_size=std::min(n,
stack.size());
160 for(std::size_t i=0; i<o.size(); i++)
171 const std::string &prefix,
180 tmp_symbol.
mode=ID_java;
181 tmp_symbol.
name=identifier;
182 tmp_symbol.
type=type;
186 result.set(ID_C_base_name, base_name);
232 result.set(ID_C_base_name, base_name);
259 const std::string &descriptor,
261 const std::string &class_name,
262 const std::string &method_name,
276 INVARIANT(member_type_from_descriptor.
id()==ID_code,
"Must be code type");
277 if(signature.has_value())
284 INVARIANT(member_type_from_signature.
id()==ID_code,
"Must be code type");
293 message.
warning() <<
"Method: " << class_name <<
"." << method_name
294 <<
"\n signature: " << signature.value()
295 <<
"\n descriptor: " << descriptor
296 <<
"\n different number of parameters, reverting to " 303 message.
warning() <<
"Method: " << class_name <<
"." << method_name
304 <<
"\n could not parse signature: " << signature.value()
305 <<
"\n " << e.what() <<
"\n" 306 <<
" reverting to descriptor: " << descriptor
323 const symbol_exprt &lambda_method_handle = lambda_method_handles.at(index);
356 method_symbol.
name=method_identifier;
358 method_symbol.
mode=ID_java;
372 member_type.
set(ID_is_synchronized,
true);
374 member_type.
set(ID_is_static,
true);
386 this_p.
type()=object_ref_type;
388 parameters.insert(parameters.begin(), this_p);
414 type_checked_cast<annotated_typet>(static_cast<typet &>(member_type))
418 method_symbol.
type=member_type;
426 method_symbol.
type.
set(ID_C_must_not_throw,
true);
429 symbol_table.
add(method_symbol);
449 method_type.
set(ID_C_class, class_symbol.
name);
457 debug() <<
"Generating codet: class " 458 << class_symbol.
name <<
", method " 475 if(v.signature.has_value())
485 std::ostringstream id_oss;
489 result.set(ID_C_base_name, v.name);
498 newv.start_pc=v.start_pc;
499 newv.length=v.length;
506 std::size_t param_index=0;
507 for(
const auto ¶m : parameters)
514 "java_parameter_count and local computation must agree");
518 for(
auto ¶m : parameters)
527 if(param_index==0 && param.get_this())
536 base_name=
variables[param_index][0].symbol_expr.get(ID_C_base_name);
537 identifier=
variables[param_index][0].symbol_expr.get(ID_identifier);
540 if(base_name.
empty())
545 const typet &type=param.type();
551 param.set_base_name(base_name);
552 param.set_identifier(identifier);
557 parameter_symbol.
mode=ID_java;
558 parameter_symbol.
name=identifier;
559 parameter_symbol.
type=param.type();
564 variables[param_index][0].is_parameter=
true;
566 variables[param_index][0].length=std::numeric_limits<size_t>::max();
574 "java_parameter_count and local computation must agree");
578 method_symbol.
name == method_identifier,
579 "Name of method symbol shouldn't change");
582 "Base name of method symbol shouldn't change");
585 "Method symbol shouldn't have module");
587 method_symbol.
mode=ID_java;
609 "Member type should have already been marked as a constructor");
617 method_symbol.
type = method_type;
630 if(statement==p->mnemonic)
633 error() <<
"failed to find bytecode mnemonic `" 634 << statement <<
'\'' <<
eom;
653 throw "unhandled java comparison instruction";
666 fieldref.
get(ID_component_name),
687 if(g.get_destination()==old_label)
688 g.set_destination(new_label);
715 unsigned address_start,
716 unsigned address_limit,
717 unsigned next_block_start_address)
725 next_block_start_address,
747 unsigned address_start,
748 unsigned address_limit,
749 unsigned next_block_start_address,
759 assert(!tree.
branch.empty());
762 const auto afterstart=
768 auto findstart=afterstart;
779 unsigned findlim_block_start_address=
781 next_block_start_address :
790 auto child_iter=this_block.
operands().begin();
793 while(child_iter!=this_block.
operands().end() &&
796 assert(child_iter!=this_block.
operands().end());
797 std::advance(child_iter, child_offset);
798 assert(child_iter!=this_block.
operands().end());
802 bool single_child(afterstart==findlim);
807 tree.
branch[child_offset],
811 findlim_block_start_address,
829 auto checkit=amap.
find(*findstart);
830 assert(checkit!=amap.end());
833 checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
836 for(
auto p : checkit->second.predecessors)
838 if(p<(*findstart) || p>=findlim_block_start_address)
840 debug() <<
"Generating codet: " 841 <<
"warning: refusing to create lexical block spanning " 842 << (*findstart) <<
"-" << findlim_block_start_address
843 <<
" due to incoming edge " << p <<
" -> " 844 << checkit->first <<
eom;
854 const irep_idt child_label_name=child_label.get_label();
855 std::string new_label_str =
id2string(child_label_name);
857 irep_idt new_label_irep(new_label_str);
861 auto nblocks=std::distance(findstart, findlim);
863 debug() <<
"Generating codet: combining " 864 << std::distance(findstart, findlim)
865 <<
" blocks for addresses " << (*findstart) <<
"-" 866 << findlim_block_start_address <<
eom;
869 auto &this_block_children=this_block.
operands();
870 assert(tree.
branch.size()==this_block_children.size());
871 for(
auto blockidx=child_offset, blocklim=child_offset+nblocks;
882 auto delfirst=this_block_children.begin();
883 std::advance(delfirst, child_offset+1);
884 auto dellim=delfirst;
885 std::advance(dellim, nblocks-1);
886 this_block_children.erase(delfirst, dellim);
887 this_block_children[child_offset].swap(newlabel);
891 auto branchstart=tree.
branch.begin();
892 std::advance(branchstart, child_offset);
893 auto branchlim=branchstart;
894 std::advance(branchlim, nblocks);
895 for(
auto branchiter=branchstart; branchiter!=branchlim; ++branchiter)
896 newnode.
branch.push_back(std::move(*branchiter));
898 tree.
branch.erase(branchstart, branchlim);
900 assert(tree.
branch.size()==this_block_children.size());
903 std::advance(branchaddriter, child_offset);
904 auto branchaddrlim=branchaddriter;
905 std::advance(branchaddrlim, nblocks);
914 tree.
branch[child_offset]=std::move(newnode);
921 to_code(this_block_children[child_offset])).code());
927 std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
929 if(e.
id()==ID_symbol)
932 auto findit = result.insert(
934 auto &var=findit.first->second;
937 var.symbol_expr=symexpr;
945 var.length+=(var.start_pc-pc);
950 var.length=std::max(var.length, (pc-var.start_pc)+1);
975 ret.
function() = findit->second.symbol_expr();
984 if(ty.
id()==ID_pointer)
1003 std::set<unsigned> targets;
1005 std::vector<unsigned> jsr_ret_targets;
1006 std::vector<instructionst::const_iterator> ret_instructions;
1008 for(
auto i_it = instructions.begin(); i_it != instructions.end(); i_it++)
1011 std::pair<address_mapt::iterator, bool> a_entry=
1012 address_map.insert(std::make_pair(i_it->address, ins));
1013 assert(a_entry.second);
1016 assert(a_entry.first==--address_map.end());
1018 if(i_it->statement!=
"goto" &&
1019 i_it->statement!=
"return" &&
1020 !(i_it->statement==
patternt(
"?return")) &&
1021 i_it->statement!=
"athrow" &&
1022 i_it->statement!=
"jsr" &&
1023 i_it->statement!=
"jsr_w" &&
1024 i_it->statement!=
"ret")
1026 instructionst::const_iterator next=i_it;
1027 if(++next!=instructions.end())
1028 a_entry.first->second.successors.push_back(next->address);
1031 if(i_it->statement==
"athrow" ||
1032 i_it->statement==
"putfield" ||
1033 i_it->statement==
"getfield" ||
1034 i_it->statement==
"checkcast" ||
1035 i_it->statement==
"newarray" ||
1036 i_it->statement==
"anewarray" ||
1037 i_it->statement==
"idiv" ||
1038 i_it->statement==
"ldiv" ||
1039 i_it->statement==
"irem" ||
1040 i_it->statement==
"lrem" ||
1041 i_it->statement==
patternt(
"?astore") ||
1042 i_it->statement==
patternt(
"?aload") ||
1043 i_it->statement==
"invokestatic" ||
1044 i_it->statement==
"invokevirtual" ||
1045 i_it->statement==
"invokespecial" ||
1046 i_it->statement==
"invokeinterface" ||
1048 i_it->statement==
"monitorexit")))
1050 const std::vector<unsigned int> handler =
1052 std::list<unsigned int> &successors = a_entry.first->second.successors;
1053 successors.insert(successors.end(), handler.begin(), handler.end());
1054 targets.insert(handler.begin(), handler.end());
1057 if(i_it->statement==
"goto" ||
1058 i_it->statement==
patternt(
"if_?cmp??") ||
1059 i_it->statement==
patternt(
"if??") ||
1060 i_it->statement==
"ifnonnull" ||
1061 i_it->statement==
"ifnull" ||
1062 i_it->statement==
"jsr" ||
1063 i_it->statement==
"jsr_w")
1070 targets.insert(target);
1072 a_entry.first->second.successors.push_back(target);
1074 if(i_it->statement==
"jsr" ||
1075 i_it->statement==
"jsr_w")
1077 auto next = std::next(i_it);
1079 next != instructions.end(),
"jsr should have valid return address");
1080 targets.insert(next->address);
1081 jsr_ret_targets.push_back(next->address);
1084 else if(i_it->statement==
"tableswitch" ||
1085 i_it->statement==
"lookupswitch")
1088 for(
const auto &arg : i_it->args)
1095 targets.insert(target);
1096 a_entry.first->second.successors.push_back(target);
1101 else if(i_it->statement==
"ret")
1104 ret_instructions.push_back(i_it);
1109 for(
const auto &address : address_map)
1111 for(
unsigned s : address.second.successors)
1113 const auto a_it = address_map.find(s);
1115 a_it->second.predecessors.insert(address.first);
1129 std::set<unsigned> working_set;
1131 if(!instructions.empty())
1132 working_set.insert(instructions.front().address);
1134 while(!working_set.empty())
1136 auto cur = working_set.begin();
1137 auto address_it = address_map.find(*cur);
1139 auto &instruction = address_it->second;
1140 unsigned cur_pc=*cur;
1141 working_set.erase(cur);
1143 if(instruction.done)
1146 instruction.successors.begin(), instruction.successors.end());
1148 instructionst::const_iterator i_it = instruction.source;
1149 stack.swap(instruction.stack);
1150 instruction.stack.clear();
1151 codet &c = instruction.code;
1154 stack.empty() || instruction.predecessors.size() <= 1 ||
1157 irep_idt statement=i_it->statement;
1164 if(statement.
size()>=2 &&
1165 statement[statement.
size()-2]==
'_' &&
1166 isdigit(statement[statement.
size()-1]))
1173 statement=std::string(
id2string(statement), 0, statement.size()-2);
1184 if(cur_pc==it->handler_pc)
1192 catch_type=it->catch_type;
1196 codet catch_instruction;
1198 if(catch_type!=
typet())
1212 stack.push_back(catch_var);
1214 catch_instruction=catch_statement;
1221 if(statement==
"aconst_null")
1223 assert(results.size()==1);
1226 else if(statement==
"athrow")
1231 else if(statement==
"checkcast")
1239 else if(statement==
"invokedynamic")
1244 lambda_method_handles, i_it->source_location, arg0))
1250 else if(statement==
"invokestatic" &&
1252 "java::org.cprover.CProver.assume:(Z)V")
1257 "function expected to have exactly one parameter");
1261 else if(statement ==
"invokestatic" &&
1262 arg0.
get(ID_identifier) ==
1263 "java::org.cprover.CProver.atomicBegin:()V")
1265 c =
codet(ID_atomic_begin);
1268 else if(statement ==
"invokestatic" &&
1269 arg0.
get(ID_identifier) ==
1270 "java::org.cprover.CProver.atomicEnd:()V")
1272 c =
codet(ID_atomic_end);
1274 else if(statement==
"invokeinterface" ||
1275 statement==
"invokespecial" ||
1276 statement==
"invokevirtual" ||
1277 statement==
"invokestatic")
1279 convert_invoke(i_it->source_location, statement, arg0, c, results);
1281 else if(statement==
"return")
1286 else if(statement==
patternt(
"?return"))
1296 else if(statement==
patternt(
"?astore"))
1298 assert(op.size()==3 && results.empty());
1301 else if(statement==
patternt(
"?store"))
1308 else if(statement==
patternt(
"?aload"))
1313 else if(statement==
patternt(
"?load"))
1319 else if(statement==
"ldc" || statement==
"ldc_w" ||
1320 statement==
"ldc2" || statement==
"ldc2_w")
1325 arg0.
id() != ID_java_string_literal && arg0.
id() != ID_type,
1326 "String and Class literals should have been lowered in " 1327 "generate_constant_global_variables");
1331 else if(statement==
"goto" || statement==
"goto_w")
1336 INVARIANT(!ret,
"goto argument should be an integer");
1340 else if(statement==
"jsr" || statement==
"jsr_w")
1346 INVARIANT(!ret,
"jsr argument should be an integer");
1351 std::next(i_it)->address,
1355 else if(statement==
"ret")
1361 assert(!jsr_ret_targets.empty());
1365 else if(statement==
"iconst_m1")
1367 assert(results.size()==1);
1370 else if(statement==
patternt(
"?const"))
1372 assert(results.size()==1);
1375 else if(statement==
patternt(
"?ipush"))
1379 arg0.
id()==ID_constant,
1380 "ipush argument expected to be constant");
1385 else if(statement==
patternt(
"if_?cmp??"))
1390 INVARIANT(!ret,
"if_?cmp?? argument should be an integer");
1392 address_map, statement, op, number, i_it->source_location);
1394 else if(statement==
patternt(
"if??"))
1397 statement==
"ifeq"?ID_equal:
1398 statement==
"ifne"?ID_notequal:
1399 statement==
"iflt"?ID_lt:
1400 statement==
"ifge"?ID_ge:
1401 statement==
"ifgt"?ID_gt:
1402 statement==
"ifle"?ID_le:
1405 INVARIANT(!
id.empty(),
"unexpected bytecode-if");
1409 INVARIANT(!ret,
"if?? argument should be an integer");
1410 c =
convert_if(address_map, op,
id, number, i_it->source_location);
1412 else if(statement==
patternt(
"ifnonnull"))
1417 INVARIANT(!ret,
"ifnonnull argument should be an integer");
1420 else if(statement==
patternt(
"ifnull"))
1425 INVARIANT(!ret,
"ifnull argument should be an integer");
1426 c =
convert_ifnull(address_map, op, number, i_it->source_location);
1428 else if(statement==
"iinc")
1432 else if(statement==
patternt(
"?xor"))
1437 else if(statement==
patternt(
"?or"))
1442 else if(statement==
patternt(
"?and"))
1447 else if(statement==
patternt(
"?shl"))
1452 else if(statement==
patternt(
"?shr"))
1457 else if(statement==
patternt(
"?ushr"))
1462 else if(statement==
patternt(
"?add"))
1467 else if(statement==
patternt(
"?sub"))
1472 else if(statement==
patternt(
"?div"))
1477 else if(statement==
patternt(
"?mul"))
1482 else if(statement==
patternt(
"?neg"))
1487 else if(statement==
patternt(
"?rem"))
1490 if(statement==
"frem" || statement==
"drem")
1495 else if(statement==
patternt(
"?cmp"))
1500 else if(statement==
patternt(
"?cmp?"))
1505 else if(statement==
patternt(
"?cmpl"))
1510 else if(statement==
"dup")
1513 results[0]=results[1]=op[0];
1515 else if(statement==
"dup_x1")
1522 else if(statement==
"dup_x2")
1532 else if(statement==
"dup2")
1537 else if(statement==
"dup2_x1")
1542 else if(statement==
"dup2_x2")
1547 else if(statement==
"dconst")
1551 else if(statement==
"fconst")
1555 else if(statement==
"getfield")
1560 else if(statement==
"getstatic")
1564 const auto &field_name=arg0.
get_string(ID_component_name);
1565 const bool is_assertions_disabled_field=
1566 field_name.find(
"$assertionsDisabled")!=std::string::npos;
1568 symbol_expr.set_identifier(
1573 "getstatic symbol should have been created before method conversion");
1576 arg0, symbol_expr, is_assertions_disabled_field, c, results);
1578 else if(statement==
"putfield")
1583 else if(statement==
"putstatic")
1587 const auto &field_name=arg0.
get_string(ID_component_name);
1588 symbol_expr.set_identifier(
1593 "putstatic symbol should have been created before method conversion");
1597 else if(statement==
patternt(
"?2?"))
1602 if(results[0].type()!=type)
1603 results[0].make_typecast(type);
1605 else if(statement==
"new")
1609 convert_new(i_it->source_location, arg0, c, results);
1611 else if(statement==
"newarray" ||
1612 statement==
"anewarray")
1618 else if(statement==
"multianewarray")
1624 INVARIANT(!ret,
"multianewarray argument should be an integer");
1628 assert(results.size()==1);
1631 else if(statement==
"arraylength")
1638 assert(pointer.type().subtype().id()==ID_symbol);
1639 array.
set(ID_java_member_access,
true);
1645 else if(statement==
"tableswitch" ||
1646 statement==
"lookupswitch")
1649 c =
convert_switch(address_map, op, i_it->args, i_it->source_location);
1651 else if(statement==
"pop" || statement==
"pop2")
1655 else if(statement==
"instanceof")
1662 else if(statement ==
"monitorenter" || statement ==
"monitorexit")
1666 else if(statement==
"swap")
1672 else if(statement==
"nop")
1687 if(catch_instruction!=
codet())
1693 if(!i_it->source_location.get_line().empty())
1698 instruction.done =
true;
1699 for(
const unsigned address : instruction.successors)
1701 address_mapt::iterator a_it2=address_map.find(address);
1707 if(address==exception_row.handler_pc)
1714 if(!
stack.empty() && a_it2->second.predecessors.size()>1)
1721 if(a_it2->second.stack.empty())
1723 for(stackt::iterator s_it=
stack.begin();
1737 a_it2->second.stack.size() ==
stack.size(),
1738 "Stack sizes should be the same.");
1739 stackt::const_iterator os_it=a_it2->second.stack.begin();
1740 for(
auto &expr :
stack)
1742 assert(
has_prefix(os_it->get_string(ID_C_base_name),
"$stack"));
1761 if(last_statement.get_statement()==ID_goto)
1766 last_statement.operands().begin(),
1775 a_it2->second.stack=
stack;
1785 new_symbol.
name=var.get_identifier();
1786 new_symbol.
type=var.type();
1787 new_symbol.
base_name=var.get(ID_C_base_name);
1789 new_symbol.
mode=ID_java;
1806 bool start_new_block=
true;
1807 bool has_seen_previous_address=
false;
1808 unsigned previous_address=0;
1809 for(
const auto &address_pair : address_map)
1811 const unsigned address=address_pair.first;
1812 assert(address_pair.first==address_pair.second.source->address);
1813 const codet &c=address_pair.second.code;
1816 if(!start_new_block)
1817 start_new_block=targets.find(address)!=targets.end();
1820 if(!start_new_block)
1821 start_new_block=address_pair.second.predecessors.size()>1;
1823 if(!start_new_block && has_seen_previous_address)
1826 if(exception_row.start_pc==previous_address)
1828 start_new_block=
true;
1840 "Block addresses should be unique and increasing");
1848 add_to_block.
add(c);
1850 start_new_block=address_pair.second.successors.size()>1;
1852 previous_address=address;
1853 has_seen_previous_address=
true;
1857 std::map<irep_idt, variablet> temporary_variable_live_ranges;
1858 for(
const auto &aentry : address_map)
1862 temporary_variable_live_ranges);
1864 std::vector<const variablet*> vars_to_process;
1866 for(
const auto &v : vlist)
1867 vars_to_process.push_back(&v);
1870 vars_to_process.push_back(
1871 &temporary_variable_live_ranges.at(v.get_identifier()));
1874 vars_to_process.push_back(
1875 &temporary_variable_live_ranges.at(v.get_identifier()));
1877 for(
const auto vp : vars_to_process)
1891 v.start_pc+v.length,
1892 std::numeric_limits<unsigned>::max(),
1895 for(
const auto vp : vars_to_process)
1901 if(v.symbol_expr.get_identifier().empty())
1907 v.start_pc+v.length,
1908 std::numeric_limits<unsigned>::max());
1910 block.operands().insert(block.operands().begin(), d);
1913 for(
auto &block : root_block.
operands())
1944 code_switch.
value() = op[0];
1948 bool is_label =
true;
1949 for(
auto a_it = args.begin(); a_it != args.end();
1950 a_it++, is_label = !is_label)
1967 if(a_it == args.begin())
1979 code_block.
add(code_case);
1983 code_switch.
body() = code_block;
1992 const irep_idt descriptor = (statement ==
"monitorenter") ?
1993 "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" :
1994 "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
2005 call.lhs().make_nil();
2006 call.arguments().push_back(op[0]);
2007 call.add_source_location() = source_location;
2022 results.insert(results.end(), op.begin(), op.end());
2023 results.insert(results.end(), op.begin(), op.end());
2035 results.insert(results.end(), op.begin() + 1, op.end());
2036 results.insert(results.end(), op.begin(), op.end());
2055 results.insert(results.end(), op.begin(), op.end());
2056 results.insert(results.end(), op2.begin(), op2.end());
2057 results.insert(results.end(), op.begin(), op.end());
2065 const char type_char = statement[0];
2066 const bool is_double(
'd' == type_char);
2067 const bool is_float(
'f' == type_char);
2069 if(is_double || is_float)
2076 if(arg0.
type().
id() != ID_floatbv)
2106 const bool use_this(statement !=
"invokestatic");
2107 const bool is_virtual(
2108 statement ==
"invokevirtual" || statement ==
"invokeinterface");
2115 if(parameters.empty() || !parameters[0].get_this())
2121 if(statement ==
"invokespecial")
2130 method_type.
set(ID_java_super_method_call,
true);
2136 parameters.insert(parameters.begin(), this_p);
2151 this_arg.
type().
id() == ID_pointer,
"first argument must be a pointer");
2159 for(std::size_t i = 0; i < parameters.size(); i++)
2161 const typet &type = parameters[i].type();
2165 type.
id() == ID_pointer)
2169 call.
arguments()[i].make_typecast(type);
2177 if(return_type.
id() != ID_empty)
2183 results[0] = promoted;
2186 assert(arg0.
id() == ID_virtual_function);
2216 symbol.
type.
set(ID_access, ID_public);
2218 symbol.
mode = ID_java;
2222 debug() <<
"Generating codet: new opaque symbol: method '" << symbol.
name 2262 c = std::move(ret_block);
2294 c = std::move(assert_class);
2307 "java::java.lang.AssertionError")
2316 assert_location.
set(
"user-provided",
true);
2323 assume_location.
set(
"user-provided",
true);
2342 const std::set<unsigned int> &working_set,
2343 unsigned int cur_pc,
2346 std::vector<irep_idt> exception_ids;
2347 std::vector<irep_idt> handler_labels;
2354 std::size_t
pos = 0;
2355 std::size_t end_pc = 0;
2372 exception_ids.push_back(
2377 handler_labels.push_back(
2385 if(!exception_ids.empty())
2389 exception_ids.size() == handler_labels.size(),
2390 "Exception tags and handler labels should be 1-to-1");
2393 for(
size_t i = 0; i < exception_ids.size(); ++i)
2395 exception_list.push_back(
2397 exception_ids[i], handler_labels[i]));
2413 exception_ids.clear();
2414 handler_labels.clear();
2418 size_t start_pc = 0;
2421 bool first_handler =
false;
2427 cur_pc < exception_row.end_pc && !working_set.empty() &&
2428 *working_set.begin() == exception_row.end_pc)
2432 if(exception_row.start_pc != start_pc || !first_handler)
2435 first_handler =
true;
2438 start_pc = exception_row.start_pc;
2461 java_new_array.operands() = op;
2475 c = std::move(create);
2489 if(statement ==
"newarray")
2495 else if(
id == ID_char)
2497 else if(
id == ID_float)
2499 else if(
id == ID_double)
2501 else if(
id == ID_byte)
2503 else if(
id == ID_short)
2505 else if(
id == ID_int)
2507 else if(
id == ID_long)
2544 java_new_expr.add_source_location() = location;
2556 c = std::move(ret_block);
2584 "stack_static_field",
2603 arg0.
get(ID_component_name));
2611 const bool is_assertions_disabled_field,
2617 if(arg0.
type().
id() == ID_symbol)
2622 else if(arg0.
type().
id() == ID_pointer)
2631 else if(is_assertions_disabled_field)
2644 else if(is_assertions_disabled_field)
2656 const int nan_value(statement[4] ==
'l' ? -1 : 1);
2706 const std::size_t width = type.
get_size_t(ID_width);
2710 if(lhs.
type() != target)
2713 if(rhs.
type() != target)
2717 if(results[0].type() != op[0].type())
2718 results[0].make_typecast(op[0].type());
2726 const unsigned address)
2741 exprt arg1_int_type = arg1;
2792 code_branch.
cond() =
2819 const typet &lhs_type(lhs.type());
2820 if(lhs_type != rhs.type())
2823 code_branch.
cond() = condition;
2834 const std::vector<unsigned int> &jsr_ret_targets,
2837 const unsigned address)
2841 for(
size_t idx = 0, idxlim = jsr_ret_targets.size(); idx != idxlim; ++idx)
2846 if(idx == idxlim - 1)
2855 branch.cond().add_source_location() = location;
2857 branch.add_source_location() = location;
2868 const char &type_char = statement[0];
2872 deref.
set(ID_java_member_access,
true);
2879 data_plus_offset.
set(ID_java_array_access,
true);
2889 const unsigned address,
2895 exprt toassign = op[0];
2896 if(
'a' == statement[0] && toassign.
type() != var.
type())
2908 assign.add_source_location() = location;
2918 const char type_char = statement[0];
2922 deref.
set(ID_java_member_access,
true);
2929 data_plus_offset.
set(ID_java_array_access,
true);
2941 block.
move(array_put);
2953 lambda_method_handles,
2954 method_type.
get_int(ID_java_lambda_method_handle_index));
2955 if(lambda_method_symbol.has_value())
2956 debug() <<
"Converting invokedynamic for lambda: " 2957 << lambda_method_symbol.value().name <<
eom;
2959 debug() <<
"Converting invokedynamic for lambda with unknown handle " 2965 pop(parameters.size());
2969 if(return_type.id() == ID_empty)
2978 const std::vector<unsigned int> &jsr_ret_targets,
2980 std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
2981 &ret_instructions)
const 2984 for(
const auto &retinst : ret_instructions)
2986 auto &a_entry = address_map.at(retinst->address);
2987 a_entry.successors.insert(
2988 a_entry.successors.end(), jsr_ret_targets.begin(), jsr_ret_targets.end());
2993 const unsigned int address,
2997 std::vector<unsigned>
result;
2998 for(
const auto &exception_row : exception_table)
3000 if(address >= exception_row.start_pc && address < exception_row.end_pc)
3001 result.push_back(exception_row.handler_pc);
3021 &local_variable_table,
3033 typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
3034 std::map<std::size_t, base_name_and_identifiert> param_names;
3035 for(
const auto &v : local_variable_table)
3037 if(v.index < slots_for_parameters)
3038 param_names.emplace(
3045 std::size_t param_index = 0;
3046 for(
auto ¶m : parameters)
3055 if(param_index == 0 && param.get_this())
3063 auto param_name = param_names.find(param_index);
3064 if(param_name != param_names.end())
3066 base_name = param_name->second.first;
3067 identifier = param_name->second.second;
3074 const typet &type = param.type();
3081 param.set_base_name(base_name);
3082 param.set_identifier(identifier);
3087 parameter_symbol.
mode = ID_java;
3088 parameter_symbol.
name = identifier;
3089 parameter_symbol.
type = param.type();
3090 symbol_table.
insert(parameter_symbol);
3101 size_t max_array_length,
3102 bool throw_assertion_error,
3106 bool threading_support)
3109 if(std::regex_match(
3111 std::regex(
".*org\\.cprover\\.CProver.*")) &&
3123 throw_assertion_error,
3124 needed_lazy_methods,
3148 return inherited_method.
is_valid();
3158 const irep_idt &component_name)
const 3169 inherited_method.
is_valid(),
"static field should be in symbol table");
3182 const std::string &tmp_var_prefix,
3183 const typet &tmp_var_type,
3188 const std::function<bool(
3189 const std::function<
tvt(
const exprt &expr)>,
const exprt &expr)>
3190 entry_matches = [&entry_matches](
3191 const std::function<tvt(const exprt &expr)> predicate,
3192 const exprt &expr) {
3193 const tvt &tvres = predicate(expr);
3199 [&predicate, &entry_matches](
const exprt &expr) {
3200 return entry_matches(predicate, expr);
3212 const std::function<tvt(const exprt &expr)> has_member_entry = [&identifier](
3213 const exprt &expr) {
3216 :
tvt(member_expr->get_component_name() == identifier);
3222 const std::function<tvt(const exprt &expr)> is_symbol_entry =
3223 [&identifier](
const exprt &expr) {
3226 :
tvt(symbol_expr->get_identifier() == identifier);
3232 const std::function<tvt(const exprt &expr)> is_dereference_entry =
3233 [](
const exprt &expr) {
3234 const auto dereference_expr =
3239 for(
auto &stack_entry :
stack)
3241 bool replace =
false;
3246 replace = entry_matches(is_symbol_entry, stack_entry);
3249 replace = entry_matches(is_dereference_entry, stack_entry);
3252 replace = entry_matches(has_member_entry, stack_entry);
3264 const std::string &tmp_var_prefix,
3265 const typet &tmp_var_type,
3269 const exprt tmp_var=
3272 stack_entry=tmp_var;
const irep_idt & get_statement() const
The type of an expression.
irep_idt name
The unique identifier.
void draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< unsigned int > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const
const codet & then_case() const
codet convert_pop(const irep_idt &statement, const exprt::operandst &op)
Fixed-width bit-vector with unsigned binary interpretation.
void set_function(const irep_idt &function)
void set_access(const irep_idt &access)
std::vector< exception_list_entryt > exception_listt
static bool is_constructor(const irep_idt &method_name)
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
JAVA Bytecode Language Conversion.
codet convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
A ‘switch’ instruction.
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
void convert(const symbolt &class_symbol, const methodt &)
std::vector< parametert > parameterst
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
pointer_typet pointer_type(const typet &subtype)
codet convert_ifnull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
std::vector< symbol_exprt > java_lambda_method_handlest
void set_label(const irep_idt &label)
dereference_exprt checked_dereference(const exprt &expr, const typet &type)
Dereference an expression and flag it for a null-pointer check.
Remove function exceptional returns.
void convert_athrow(const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const
Over-approximative uncaught exceptions analysis.
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
optionalt< std::string > signature
typet java_boolean_type()
irep_idt method_id
Fully qualified name of the method under translation.
void set_property_class(const irep_idt &property_class)
const exprt variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
Returns a symbol_exprt indicating a local variable suitable to load/store from a bytecode at address ...
static bool operator==(const irep_idt &what, const patternt &pattern)
constant_exprt to_expr() const
Non-graph-based representation of the class hierarchy.
optionalt< symbolt > get_lambda_method_symbol(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const size_t index)
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap m...
static void gather_symbol_live_ranges(unsigned pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result)
methodt::instructionst instructionst
const java_lambda_method_handlest & lambda_method_handles() const
irep_idt mode
Language mode.
const exprt & cond() const
void from_expr(const constant_exprt &expr)
bool is_method_inherited(const irep_idt &classname, const irep_idt &methodid) const
Returns true iff method methodid from class classname is a method inherited from a class (and not an ...
optionalt< ci_lazy_methods_neededt > needed_lazy_methods
code_blockt & get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address, const address_mapt &amap, bool allow_merge=true)
As above, but this version can additionally create a new branch in the block_tree-node and code_block...
reference_typet java_reference_type(const typet &subtype)
void set_comment(const irep_idt &comment)
const bool threading_support
signed int get_int(const irep_namet &name) const
static irep_idt label(const irep_idt &address)
void copy_to_operands(const exprt &expr)
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
const irep_idt & get_identifier() const
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
std::string as_string() const
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
void move_to_operands(exprt &expr)
struct bytecode_infot const bytecode_info[]
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The null pointer constant.
exprt value
Initial value of symbol.
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
The trinary if-then-else operator.
irep_idt module
Name of module the symbol belongs to.
A ‘goto’ instruction.
irep_idt pretty_name
Language-specific display name.
An exception that is raised for unsupported class signature.
Pops an exception handler from the stack of active handlers (i.e.
bool operator==(const irep_idt &what) const
codet convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, unsigned address)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::vector< unsigned int > try_catch_handler(unsigned int address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
A constant literal expression.
#define CHECK_RETURN(CONDITION)
static mstreamt & eom(mstreamt &m)
void convert_new(const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results)
bool get_is_constructor() const
bool is_parameter(const local_variablet &v)
Returns true iff the slot index of the local variable of a method (coming from the LVT) is a paramete...
std::map< unsigned, converted_instructiont > address_mapt
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
codet convert_switch(java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
expanding_vectort< variablest > variables
A side effect that throws an exception.
#define INVARIANT(CONDITION, REASON)
const exprt & case_op() const
java_method_typet member_type_lazy(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name, const std::string &method_name, message_handlert &message_handler)
Returns the member type for a method, based on signature or descriptor.
code_blockt & get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address)
'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are ...
void set_base_name(const irep_idt &name)
static ieee_float_spect double_precision()
Extract member of struct or union.
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
mstreamt & warning() const
codet convert_putfield(const exprt &arg0, const exprt::operandst &op)
irep_idt current_method
A copy of method_id :/.
void set_is_constructor()
Expression Initialization.
const irep_idt & id() const
Evaluates to true if the operand is NaN.
typet java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof...
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
class code_blockt & make_block()
void add_throws_exceptions(irep_idt exception)
static irep_idt get_if_cmp_operator(const irep_idt &stmt)
source_locationt source_location
Given a string of the format '?blah?', will return true when compared against a string that matches a...
std::vector< exceptiont > exception_tablet
const irep_idt & get_line() const
division (integer and real)
A reference into the symbol table.
A declaration of a local variable.
exprt::operandst & convert_ushr(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
exprt::operandst & convert_cmp2(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
std::vector< exprt > argst
codet replace_character_call(code_function_callt call)
Operator to dereference a pointer.
void convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
static std::size_t get_bytecode_type_width(const typet &ty)
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
nonstd::optional< T > optionalt
const code_gotot & to_code_goto(const codet &code)
exprt::operandst & convert_cmp(const exprt::operandst &op, exprt::operandst &results) const
API to expression classes.
exprt::operandst & convert_const(const irep_idt &statement, const exprt &arg0, exprt::operandst &results) const
irep_idt get_static_field(const irep_idt &class_identifier, const irep_idt &component_name) const
Get static field identifier referred to by class_identifier.component_name Note this may be inherited...
codet convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const unsigned address, const source_locationt &location)
const irep_idt & get(const irep_namet &name) const
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
static ieee_float_spect single_precision()
class_hierarchyt class_hierarchy
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support)
A label for branch targets.
#define PRECONDITION(CONDITION)
Given a class and a component (either field or method), find the closest parent that defines that com...
std::string pretty_signature(const java_method_typet &method_type)
bool has_prefix(const std::string &s, const std::string &prefix)
Base class for tree-like data structures with sharing.
#define forall_operands(it, expr)
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted), leaving the driver program to stub them if it wishes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void convert_invoke(source_locationt location, const irep_idt &statement, exprt &arg0, codet &c, exprt::operandst &results)
unsigned java_local_variable_slots(const typet &t)
Returns the number of JVM local variables (slots) taken by a local variable that, when translated to ...
const size_t max_array_length
java_string_library_preprocesst & string_preprocess
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
codet & find_last_statement()
codet get_clinit_call(const irep_idt &classname)
Each static access to classname should be prefixed with a check for necessary static init; this retur...
The unary minus expression.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
void convert_checkcast(const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const
typet method_return_type
Return type of the method under conversion.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The boolean constant false.
std::list< symbol_exprt > tmp_vars
const codet & body() const
typet java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
exprt::operandst pop(std::size_t n)
void java_bytecode_convert_method_lazy(const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_tablet &symbol_table, message_handlert &message_handler)
This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet...
std::set< symbol_exprt > used_local_names
const bool throw_assertion_error
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
std::vector< block_tree_nodet > branch
unsigned integer2unsigned(const mp_integer &n)
A non-fatal assertion, which checks a condition then permits execution to continue.
An assumption, which must hold in subsequent code.
const exprt & value() const
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
message_handlert & get_message_handler()
const java_method_typet & to_java_method_type(const typet &type)
std::vector< variablet > variablest
const bytecode_infot & get_bytecode_info(const irep_idt &statement)
void create_stack_tmp_var(const std::string &, const typet &, code_blockt &, exprt &)
actually create a temporary variable to hold the value of a stack entry
codet convert_monitorenterexit(const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location)
mstreamt & result() const
void convert_dup2_x1(exprt::operandst &op, exprt::operandst &results)
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
void convert_getstatic(const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results)
instructionst instructions
Base class for all expressions.
void convert_annotations(const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector< java_annotationt > &java_annotations)
Convert parsed annotations into the symbol table.
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
const exprt & assumption() const
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
std::vector< local_variablet > local_variable_tablet
exception_tablet exception_table
unsigned java_method_parameter_slots(const java_method_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call...
void save_stack_entries(const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &)
Create temporary variables if a write instruction can have undesired side- effects.
const std::string & get_string(const irep_namet &name) const
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
codet & replace_call_to_cprover_assume(source_locationt location, codet &c)
void from_integer(const mp_integer &i)
void push(const exprt::operandst &o)
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
codet & do_exception_handling(const methodt &method, const std::set< unsigned int > &working_set, unsigned int cur_pc, codet &c)
symbol_table_baset & symbol_table
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
Expression to hold a symbol (variable)
const code_blockt & to_code_block(const codet &code)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results)
void convert_dup2(exprt::operandst &op, exprt::operandst &results)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
goto_programt coverage_criteriont message_handlert & message_handler
A statement in a programming language.
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
unsigned slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
std::size_t integer2size_t(const mp_integer &n)
codet convert_ifnonull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
const code_labelt & to_code_label(const codet &code)
JAVA Bytecode Language Conversion.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
An expression containing a side effect.
local_variable_tablet local_variable_table
Compute dominators for CFG of goto_function.
codet convert_if(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const irep_idt &id, const mp_integer &number, const source_locationt &location) const
void java_bytecode_initialize_parameter_names(symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize sym...
void push_back(const T &t)
static void replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label)
Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.
std::size_t get_size_t(const irep_namet &name) const
exception_listt & exception_list()
optionalt< exprt > convert_invoke_dynamic(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const source_locationt &location, const exprt &arg0)
void convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
codet convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
void make_typecast(const typet &_type)
const irept & find(const irep_namet &name) const
static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
irep_idt get_full_component_identifier() const
Get the full name of this function.
codet convert_if_cmp(const java_bytecode_convert_methodt::address_mapt &address_map, const irep_idt &statement, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
std::vector< unsigned > branch_addresses
const typet & return_type() const
const java_class_typet & to_java_class_type(const typet &type)
char java_char_from_type(const typet &type)
void set(const irep_namet &name, const irep_idt &value)
exprt convert_aload(const irep_idt &statement, const exprt::operandst &op) const
static void assign_parameter_names(java_method_typet &ftype, const irep_idt &name_prefix, symbol_table_baset &symbol_table)
Iterates through the parameters of the function type ftype, finds a new new name for each parameter a...
A statement that catches an exception, assigning the exception in flight to an expression (e...
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
void branch(goto_modelt &goto_model, const irep_idt &id)
const exprt & assertion() const
Produce code for simple implementation of String Java libraries.
code_blockt convert_ret(const std::vector< unsigned int > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const unsigned address)
static block_tree_nodet get_leaf()
codet convert_instructions(const methodt &, const java_class_typet::java_lambda_method_handlest &)
IEEE-floating-point equality.
std::vector< irep_idt > throws_exception_table