35 #define INITIALIZE CPROVER_PREFIX "initialize" 42 initialize.
mode=ID_java;
58 initialize.
value=init_code;
60 if(symbol_table.
add(initialize))
61 throw "failed to add "+std::string(
INITIALIZE);
67 if(sym.
type.
id()!=ID_code &&
80 bool assume_init_pointers_not_null,
81 unsigned max_nondet_array_length)
90 std::list<irep_idt> symbol_names;
91 for(
const auto &entry : symbol_table.
symbols)
92 symbol_names.push_back(entry.first);
94 for(
const auto &symname : symbol_names)
101 bool allow_null=!assume_init_pointers_not_null;
105 const std::string suffix=
"@class_model";
111 "java::java.lang.String.Literal"))
120 max_nondet_array_length,
123 code_block.
add(assignment);
129 code_block.
add(assignment);
136 for(symbol_tablet::symbolst::const_iterator
137 it=symbol_table.
symbols.begin();
138 it!=symbol_table.
symbols.end();
141 if(it->second.base_name==
"<clinit>" &&
142 it->second.type.id()==ID_code &&
143 it->second.mode==ID_java)
147 function_call.
function()=it->second.symbol_expr();
149 code_block.
add(function_call);
158 bool assume_init_pointers_not_null,
159 unsigned max_nondet_array_length)
165 main_arguments.resize(parameters.size());
167 for(std::size_t param_number=0;
168 param_number<parameters.size();
171 bool is_this=(param_number==0) &&
172 parameters[param_number].get_this();
173 bool is_default_entry_point(
config.
main.empty());
174 bool is_main=is_default_entry_point;
178 const typet &string_array_type=
180 bool has_correct_type=
183 parameters.
size()==1 &&
184 parameters[0].type().full_eq(string_array_type);
185 is_main=(named_main && has_correct_type);
190 (
"argument#"+std::to_string(param_number)):p.
get_base_name();
192 bool allow_null=(!is_main) && (!is_this) && !assume_init_pointers_not_null;
194 main_arguments[param_number]=
201 max_nondet_array_length,
205 codet input(ID_input);
206 input.operands().resize(2);
212 input.op1()=main_arguments[param_number];
213 input.add_source_location()=
function.location;
215 init_code.move_to_operands(input);
218 return main_arguments;
231 result.reserve(parameters.size()+1);
233 bool has_return_value=
239 codet output(ID_output);
255 for(std::size_t param_number=0;
256 param_number<parameters.size();
260 symbol_table.
lookup(parameters[param_number].get_identifier());
262 if(p_symbol.
type.
id()==ID_pointer)
265 codet output(ID_output);
272 output.
op1()=main_arguments[param_number];
280 codet output(ID_output);
292 output.
op1()=exc_symbol.symbol_expr();
313 std::string main_identifier=
"java::"+
config.
main;
315 symbol_tablet::symbolst::const_iterator s_it;
320 std::string prefix=main_identifier+
':';
321 std::set<irep_idt> matches;
323 for(
const auto &s : symbol_table.
symbols)
325 s.second.type.id()==ID_code)
326 matches.insert(s.first);
337 else if(matches.size()==1)
339 s_it=symbol_table.
symbols.find(*matches.begin());
340 assert(s_it!=symbol_table.
symbols.end());
345 <<
"' is ambiguous:\n";
347 for(
const auto &s : matches)
348 message.
error() <<
" " << s <<
'\n';
360 s_it=symbol_table.
symbols.find(main_identifier);
362 if(s_it==symbol_table.
symbols.end())
375 if(symbol.
type.
id()!=ID_code)
388 message.
error() <<
"main method `" << main_class
402 if(main_class.
empty())
410 std::string entry_method=
413 std::string prefix=
"java::"+entry_method+
":";
416 std::set<irep_idt> matches;
418 for(symbol_tablet::symbolst::const_iterator
419 s_it=symbol_table.
symbols.begin();
420 s_it!=symbol_table.
symbols.end();
423 if(s_it->second.type.id()==ID_code &&
425 matches.insert(s_it->first);
437 if(matches.size()>=2)
439 message.
error() <<
"main method in `" << main_class
448 symbol=symbol_table.
symbols.find(*matches.begin())->second;
453 message.
error() <<
"main method `" << main_class
480 bool assume_init_pointers_not_null,
481 size_t max_nondet_array_length)
496 assert(symbol.
type.
id()==ID_code);
503 assume_init_pointers_not_null,
504 max_nondet_array_length);
510 symbol_tablet::symbolst::iterator init_it=
513 if(init_it==symbol_table.
symbols.end())
523 call_init.
function()=init_it->second.symbol_expr();
543 return_symbol.
mode=ID_C;
545 return_symbol.
name=
"return'";
549 symbol_table.
add(return_symbol);
555 exc_symbol.
mode=ID_C;
560 symbol_table.
add(exc_symbol);
567 assume_init_pointers_not_null,
568 max_nondet_array_length);
584 new_symbol.
mode=ID_java;
586 if(symbol_table.
move(new_symbol))
exprt::operandst java_build_arguments(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table, bool assume_init_pointers_not_null, unsigned max_nondet_array_length)
The type of an expression.
irep_idt name
The unique identifier.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
Remove function exceptional returns.
irep_idt mode
Language mode.
reference_typet java_reference_type(const typet &subtype)
const irep_idt & get_identifier() const
void move_to_operands(exprt &expr)
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, size_t max_nondet_array_length, const source_locationt &loc)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
bool java_entry_point(symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, size_t max_nondet_array_length)
find entry point and create initialization code for function symbol_table main class message_handler ...
const irep_idt & id() const
const irep_idt & get_base_name() const
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
typet java_type_from_string(const std::string &src)
static irep_idt entry_point()
API to expression classes.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
static void create_initialize(symbol_tablet &symbol_table)
void java_record_outputs(const symbolt &function, const exprt::operandst &main_arguments, code_blockt &init_code, symbol_tablet &symbol_table)
bitvector_typet index_type()
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Operator to return the address of an object.
main_function_resultt get_main_symbol(symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool allow_no_body)
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
bool has_symbol(const irep_idt &name) const
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
const code_blockt & to_code_block(const codet &code)
bool has_suffix(const std::string &s, const std::string &suffix)
A statement in a programming language.
void java_static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, unsigned max_nondet_array_length)
static bool should_init_symbol(const symbolt &sym)
const typet & return_type() const