CBMC
|
Java simple opaque stub generation. More...
#include "simple_method_stubbing.h"
#include <java_bytecode/java_object_factory.h>
#include <java_bytecode/java_object_factory_parameters.h>
#include <java_bytecode/java_pointer_casts.h>
#include <java_bytecode/java_types.h>
#include "java_utils.h"
#include <util/invariant_utils.h>
#include <util/namespace.h>
#include <util/std_code.h>
#include <util/symbol_table_base.h>
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... | |
Java simple opaque stub generation.
Definition in file simple_method_stubbing.cpp.
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.
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
.
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 294 of file simple_method_stubbing.cpp.