cprover
remove_java_new.cpp File Reference

Remove Java New Operators. More...

Include dependency graph for remove_java_new.cpp:

Go to the source code of this file.

Classes

class  remove_java_newt
 

Functions

void remove_java_new (goto_programt::targett target, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler)
 Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...
 
void remove_java_new (goto_functionst::goto_functiont &function, symbol_table_baset &symbol_table, message_handlert &message_handler)
 Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...
 
void remove_java_new (goto_functionst &goto_functions, symbol_table_baset &symbol_table, message_handlert &message_handler)
 Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...
 
void remove_java_new (goto_modelt &goto_model, message_handlert &message_handler)
 Replace every java_new or java_new_array by a malloc side-effect and zero initialization. More...
 

Detailed Description

Remove Java New Operators.

Definition in file remove_java_new.cpp.

Function Documentation

◆ remove_java_new() [1/4]

void remove_java_new ( goto_programt::targett  target,
goto_programt goto_program,
symbol_table_baset symbol_table,
message_handlert message_handler 
)

Replace every java_new or java_new_array by a malloc side-effect and zero initialization.

Remarks
Extra auxiliary variables may be introduced into symbol_table.
Parameters
targetThe instruction to work on.
goto_programThe function body containing the instruction.
symbol_tableThe symbol table to add symbols to.
message_handlera message handler

Definition at line 383 of file remove_java_new.cpp.

References goto_program, remove_java_newt::lower_java_new(), and message_handler.

Referenced by jbmc_parse_optionst::process_goto_function(), and remove_java_new().

◆ remove_java_new() [2/4]

void remove_java_new ( goto_functionst::goto_functiont function,
symbol_table_baset symbol_table,
message_handlert message_handler 
)

Replace every java_new or java_new_array by a malloc side-effect and zero initialization.

Remarks
Extra auxiliary variables may be introduced into symbol_table.
Parameters
functionThe function to work on.
symbol_tableThe symbol table to add symbols to.
message_handlera message handler

Definition at line 399 of file remove_java_new.cpp.

References remove_java_newt::lower_java_new(), and message_handler.

◆ remove_java_new() [3/4]

void remove_java_new ( goto_functionst goto_functions,
symbol_table_baset symbol_table,
message_handlert message_handler 
)

Replace every java_new or java_new_array by a malloc side-effect and zero initialization.

Remarks
Extra auxiliary variables may be introduced into symbol_table.
Parameters
goto_functionsThe functions to work on.
symbol_tableThe symbol table to add symbols to.
message_handlera message handler

Definition at line 414 of file remove_java_new.cpp.

References goto_functionst::compute_location_numbers(), goto_functionst::function_map, remove_java_newt::lower_java_new(), and message_handler.

◆ remove_java_new() [4/4]

void remove_java_new ( goto_modelt goto_model,
message_handlert message_handler 
)

Replace every java_new or java_new_array by a malloc side-effect and zero initialization.

Remarks
Extra auxiliary variables may be introduced into symbol_table.
Parameters
goto_modelThe functions to work on and the symbol table to add symbols to.
message_handlera message handler

Definition at line 433 of file remove_java_new.cpp.

References goto_modelt::goto_functions, message_handler, remove_java_new(), and goto_modelt::symbol_table.