cprover
|
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"
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) |
Expression Initialization.
Definition in file expr_initializer.cpp.
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.
exprt nondet_initializer | ( | const typet & | type, |
const source_locationt & | source_location, | ||
const namespacet & | ns | ||
) |
Definition at line 371 of file expr_initializer.cpp.
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().
exprt zero_initializer | ( | const typet & | type, |
const source_locationt & | source_location, | ||
const namespacet & | ns | ||
) |
Definition at line 352 of file expr_initializer.cpp.