cbmc/remove__java__new_8h_source.html

/*******************************************************************\


Module: Remove Java New Operators


Author: Peter Schrammel


\*******************************************************************/


#ifndef CPROVER_JAVA_BYTECODE_REMOVE_JAVA_NEW_H

#define CPROVER_JAVA_BYTECODE_REMOVE_JAVA_NEW_H


#include <goto-programs/goto_functions.h>


class goto_modelt;

class message_handlert;

class symbol_table_baset;


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);


void remove_java_new(

  const irep_idt &function_identifier,

  goto_functionst::goto_functiont &function,

  symbol_table_baset &symbol_table,

  message_handlert &_message_handler);


void remove_java_new(

  goto_functionst &goto_functions,

  symbol_table_baset &symbol_table,

  message_handlert &_message_handler);


void remove_java_new(goto_modelt &model, message_handlert &_message_handler);


#endif // CPROVER_JAVA_BYTECODE_REMOVE_JAVA_NEW_H

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38

goto_functionst
A collection of goto functions.
Definition goto_functions.h:25

goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition goto_functions.h:27

goto_modelt
Definition goto_model.h:27

goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:73

goto_programt::targett
instructionst::iterator targett
Definition goto_program.h:614

message_handlert
Definition message.h:27

symbol_table_baset
The symbol table base class interface.
Definition symbol_table_base.h:23

goto_functions.h
Goto Programs with Functions.

remove_java_new
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.
Definition remove_java_new.cpp:438