expr_initializer.cpp File Reference

Expression Initialization. More...

#include "expr_initializer.h"
#include "arith_tools.h"
#include "c_types.h"
#include "format_expr.h"
#include "format_type.h"
#include "invariant.h"
#include "message.h"
#include "namespace.h"
#include "pointer_offset_size.h"
#include "std_code.h"
#include "std_expr.h"

Include dependency graph for expr_initializer.cpp:

Go to the source code of this file.

Classes
class	expr_initializert< nondet >

Functions
exprt	zero_initializer (const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
exprt	nondet_initializer (const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
exprt	zero_initializer (const typet &type, const source_locationt &source_location, const namespacet &ns)
exprt	nondet_initializer (const typet &type, const source_locationt &source_location, const namespacet &ns)

Detailed Description

Expression Initialization.

Definition in file expr_initializer.cpp.

Function Documentation

nondet_initializer() [1/2]

exprt nondet_initializer	(	const typet &	type,
		const source_locationt &	source_location,
		const namespacet &	ns,
		message_handlert &	message_handler
	)

Definition at line 342 of file expr_initializer.cpp.

References message_handler.

nondet_initializer() [2/2]

exprt nondet_initializer	(	const typet &	type,
		const source_locationt &	source_location,
		const namespacet &	ns
	)

Definition at line 371 of file expr_initializer.cpp.

zero_initializer() [1/2]

exprt zero_initializer	(	const typet &	type,
		const source_locationt &	source_location,
		const namespacet &	ns,
		message_handlert &	message_handler
	)

Definition at line 332 of file expr_initializer.cpp.

References message_handler.

Referenced by java_bytecode_convert_methodt::convert_invoke_dynamic(), c_typecheck_baset::do_designated_initializer(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), java_object_factoryt::gen_nondet_struct_init(), get_or_create_string_literal_symbol(), java_static_lifetime_init(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), linker_script_merget::ls_data2instructions(), static_lifetime_init(), goto_symext::symex_allocate(), goto_symext::symex_gcc_builtin_va_arg_next(), and goto_symext::symex_start_thread().

zero_initializer() [2/2]

exprt zero_initializer	(	const typet &	type,
		const source_locationt &	source_location,
		const namespacet &	ns
	)

Definition at line 352 of file expr_initializer.cpp.