cprover
|
#include "java_object_factory.h"
#include <unordered_set>
#include <sstream>
#include <util/arith_tools.h>
#include <util/fresh_symbol.h>
#include <util/c_types.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/namespace.h>
#include <util/pointer_offset_size.h>
#include <util/prefix.h>
#include <linking/zero_initializer.h>
#include <goto-programs/goto_functions.h>
#include "java_types.h"
#include "java_utils.h"
Go to the source code of this file.
Classes | |
class | java_object_factoryt |
Functions | |
static symbolt & | new_tmp_symbol (symbol_tablet &symbol_table, const source_locationt &loc, const typet &type, const std::string &prefix="tmp_object_factory") |
static exprt | get_nondet_bool (const typet &type) |
exprt | object_factory (const typet &type, const irep_idt base_name, code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, size_t max_nondet_array_length, const source_locationt &loc) |
Definition at line 47 of file java_object_factory.cpp.
Referenced by java_object_factoryt::gen_nondet_init().
|
static |
Definition at line 30 of file java_object_factory.cpp.
References get_fresh_aux_symbol().
Referenced by java_object_factoryt::allocate_nondet_length_array(), java_object_factoryt::allocate_object(), and java_object_factoryt::gen_nondet_array_init().
exprt object_factory | ( | const typet & | type, |
const irep_idt | base_name, | ||
code_blockt & | init_code, | ||
bool | allow_null, | ||
symbol_tablet & | symbol_table, | ||
size_t | max_nondet_array_length, | ||
const source_locationt & | loc | ||
) |
Definition at line 610 of file java_object_factory.cpp.
References code_blockt::add(), exprt::add_source_location(), code_blockt::append(), symbolt::base_name, goto_functions_templatet< goto_programt >::entry_point(), java_object_factoryt::gen_nondet_init(), id2string(), symbolt::is_static_lifetime, java_object_factoryt::loc, symbolt::location, symbolt::mode, symbol_tablet::move(), symbolt::name, symbolt::symbol_expr(), java_object_factoryt::symbols_created, and symbolt::type.
Referenced by java_build_arguments(), and java_static_lifetime_init().