cprover
|
#include <util/cprover_prefix.h>
Go to the source code of this file.
Macros | |
#define | INITIALIZE_FUNCTION CPROVER_PREFIX "initialize" |
Functions | |
bool | static_lifetime_init (symbol_tablet &symbol_table, const source_locationt &source_location, message_handlert &message_handler) |
#define INITIALIZE_FUNCTION CPROVER_PREFIX "initialize" |
Definition at line 24 of file static_lifetime_init.h.
Referenced by linker_script_merget::add_linker_script_definitions(), ansi_c_internal_additions(), jbmc_parse_optionst::can_generate_function_body(), dump_ct::cleanup_harness(), symex_coveraget::compute_overall_coverage(), cpp_internal_additions(), create_initialize(), aggressive_slicert::doit(), generate_ansi_c_start_function(), generate_java_start_function(), interrupt(), java_static_lifetime_init(), jsil_entry_point(), compilet::link(), list_calls_and_arguments(), mmio(), nondet_static(), code_contractst::operator()(), internal_functions_filtert::operator()(), print_global_state_size(), race_check(), remove_internal_symbols(), bmct::setup(), slice_global_inits(), stack_depth(), static_lifetime_init(), instrumentert::cfg_visitort::visit_cfg_function(), weak_memory(), and shared_bufferst::cfg_visitort::weak_memory().
bool static_lifetime_init | ( | symbol_tablet & | symbol_table, |
const source_locationt & | source_location, | ||
message_handlert & | message_handler | ||
) |
Definition at line 25 of file static_lifetime_init.cpp.
References code_blockt::add(), exprt::add_source_location(), CPROVER_PREFIX, namespace_baset::follow(), from_integer(), code_function_callt::function(), symbol_tablet::get_writeable(), has_prefix(), irept::id(), id2string(), INITIALIZE_FUNCTION, symbolt::is_extern, symbolt::is_macro, irept::is_nil(), irept::is_not_nil(), symbolt::is_static_lifetime, symbolt::is_type, symbolt::location, namespacet::lookup(), message_handler, exprt::move_to_operands(), symbolt::name, code_typet::parameters(), code_typet::return_type(), irept::set(), array_typet::size(), size_type(), symbolt::symbol_expr(), symbol_table_baset::symbols, to_array_type(), to_code(), to_code_block(), to_code_type(), symbolt::type, symbolt::value, and zero_initializer().
Referenced by ansi_c_entry_point().