CBMC
Loading...
Searching...
No Matches
Classes | Functions
remove_java_new.cpp File Reference

Remove Java New Operators. More...

#include "remove_java_new.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/expr_initializer.h>
#include <util/namespace.h>
#include <util/pointer_offset_size.h>
#include <util/std_code.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_model.h>
#include <ansi-c/goto-conversion/goto_convert.h>
#include "java_types.h"
#include "java_utils.h"
+ 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 (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.
 
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.
 
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.
 
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.
 

Detailed Description

Remove Java New Operators.

Definition in file remove_java_new.cpp.

Function Documentation

◆  remove_java_new() [1/4]

void remove_java_new ( const irep_idtfunction_identifier,
symbol_table_basetsymbol_table,
message_handlertmessage_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_identifier Name of the function function.
function The function to work on.
symbol_table The symbol table to add symbols to.
message_handler a message handler

Definition at line 457 of file remove_java_new.cpp.

◆  remove_java_new() [2/4]

void remove_java_new ( const irep_idtfunction_identifier,
goto_programtgoto_program,
symbol_table_basetsymbol_table,
message_handlertmessage_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_identifier Name of the function containing target.
target The instruction to work on.
goto_program The function body containing the instruction.
symbol_table The symbol table to add symbols to.
message_handler a message handler

Definition at line 438 of file remove_java_new.cpp.

◆  remove_java_new() [3/4]

void remove_java_new ( goto_functionstgoto_functions,
symbol_table_basetsymbol_table,
message_handlertmessage_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_functions The functions to work on.
symbol_table The symbol table to add symbols to.
message_handler a message handler

Definition at line 473 of file remove_java_new.cpp.

◆  remove_java_new() [4/4]

void remove_java_new ( goto_modeltgoto_model,
message_handlertmessage_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_model The functions to work on and the symbol table to add symbols to.
message_handler a message handler

Definition at line 493 of file remove_java_new.cpp.

AltStyle によって変換されたページ (->オリジナル) /