CBMC
remove_java_new.h File Reference

Remove Java New Operators. More...

+ Include dependency graph for remove_java_new.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void remove_java_new (const irep_idt &function_identifier, 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 (const irep_idt &function_identifier, 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 &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.h.

Function Documentation

◆ remove_java_new() [1/4]

void remove_java_new ( const irep_idt function_identifier,
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
function_identifierName of the function function.
functionThe function to work on.
symbol_tableThe symbol table to add symbols to.
message_handlera message handler

Definition at line 457 of file remove_java_new.cpp.

◆ remove_java_new() [2/4]

void remove_java_new ( const irep_idt function_identifier,
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
function_identifierName of the function containing target.
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 438 of file remove_java_new.cpp.

◆ 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 473 of file remove_java_new.cpp.

◆ 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 493 of file remove_java_new.cpp.