cprover
|
Java simple opaque stub generation. More...
#include <util/irep.h>
Go to the source code of this file.
Functions | |
void | java_generate_simple_method_stub (const irep_idt &function_name, symbol_table_baset &symbol_table, bool assume_non_null, const 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 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... | |
Java simple opaque stub generation.
Definition in file simple_method_stubbing.h.
void java_generate_simple_method_stub | ( | const irep_idt & | function_name, |
symbol_table_baset & | symbol_table, | ||
bool | assume_non_null, | ||
const object_factory_parameterst & | object_factory_parameters, | ||
message_handlert & | message_handler | ||
) |
Definition at line 245 of file simple_method_stubbing.cpp.
References java_simple_method_stubst::check_method_stub(), and message_handler.
Referenced by jbmc_parse_optionst::generate_function_body().
void java_generate_simple_method_stubs | ( | symbol_table_baset & | symbol_table, |
bool | assume_non_null, | ||
const 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
.
symbol_table | Global symbol table |
assume_non_null | If true, generated function stubs will never initialize reference members with null. |
object_factory_parameters | specifies exactly how nondet composite objects should be created– for example, object graph depth. |
message_handler | Logging |
Definition at line 267 of file simple_method_stubbing.cpp.
References java_simple_method_stubst::check_method_stub(), message_handler, and symbol_table_baset::symbols.