CBMC
simple_method_stubbing.cpp File Reference

Java simple opaque stub generation. More...

+ Include dependency graph for simple_method_stubbing.cpp:

Go to the source code of this file.

Classes

class  java_simple_method_stubst
 

Functions

void java_generate_simple_method_stub (const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const java_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
 
void java_generate_simple_method_stubs (symbol_table_baset &symbol_table, bool assume_non_null, const java_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
 Generates function stubs for most undefined functions in the symbol table, except as forbidden in java_simple_method_stubst::check_method_stub. More...
 

Detailed Description

Java simple opaque stub generation.

Definition in file simple_method_stubbing.cpp.

Function Documentation

◆ java_generate_simple_method_stub()

void java_generate_simple_method_stub ( const irep_idt function_name,
symbol_table_baset symbol_table,
bool  assume_non_null,
const java_object_factory_parameterst object_factory_parameters,
message_handlert message_handler 
)

Definition at line 272 of file simple_method_stubbing.cpp.

◆ java_generate_simple_method_stubs()

void java_generate_simple_method_stubs ( symbol_table_baset symbol_table,
bool  assume_non_null,
const java_object_factory_parameterst object_factory_parameters,
message_handlert message_handler 
)

Generates function stubs for most undefined functions in the symbol table, except as forbidden in java_simple_method_stubst::check_method_stub.

Parameters
symbol_tableGlobal symbol table
assume_non_nullIf true, generated function stubs will never initialize reference members with null.
object_factory_parametersspecifies exactly how nondet composite objects should be created– for example, object graph depth.
message_handlerLogging

Definition at line 294 of file simple_method_stubbing.cpp.