cprover
|
Expression Initialization. More...
#include "expr.h"
Go to the source code of this file.
Functions | |
exprt | zero_initializer (const typet &, const source_locationt &, const namespacet &, message_handlert &) |
exprt | nondet_initializer (const typet &, const source_locationt &, const namespacet &, message_handlert &) |
exprt | zero_initializer (const typet &, const source_locationt &, const namespacet &) |
exprt | nondet_initializer (const typet &type, const source_locationt &source_location, const namespacet &ns) |
Expression Initialization.
Definition in file expr_initializer.h.
exprt nondet_initializer | ( | const typet & | , |
const source_locationt & | , | ||
const namespacet & | , | ||
message_handlert & | |||
) |
Definition at line 354 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 383 of file expr_initializer.cpp.
exprt zero_initializer | ( | const typet & | , |
const source_locationt & | , | ||
const namespacet & | , | ||
message_handlert & | |||
) |
Definition at line 344 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 & | , |
const source_locationt & | , | ||
const namespacet & | |||
) |
Definition at line 364 of file expr_initializer.cpp.