java_object_factory.cpp File Reference

#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"

Include dependency graph for java_object_factory.cpp:

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)

Function Documentation

get_nondet_bool()

static exprt get_nondet_bool ( const typet &  type )

static

parameters: Desired type (C_bool or plain bool)

Returns

nondet expr of that type

Definition at line 47 of file java_object_factory.cpp.

Referenced by java_object_factoryt::gen_nondet_init().

new_tmp_symbol()

static symbolt& new_tmp_symbol ( symbol_tablet &  symbol_table, const source_locationt &  loc, const typet &  type, const std::string &  prefix = "tmp_object_factory"  )

static

Definition at line 30 of file java_object_factory.cpp.

References get_fresh_aux_symbol(), and loc.

Referenced by java_object_factoryt::allocate_nondet_length_array(), java_object_factoryt::allocate_object(), and java_object_factoryt::gen_nondet_array_init().

object_factory()

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, loc, symbolt::location, symbolt::mode, symbol_tablet::move(), symbolt::name, symbolt::symbol_expr(), and symbolt::type.

Referenced by java_build_arguments(), and java_static_lifetime_init().