cprover
|
#include <util/symbol_table.h>
#include <util/message.h>
#include <util/source_location.h>
#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 23 of file static_lifetime_init.h.
Referenced by ansi_c_entry_point(), and static_lifetime_init().
bool static_lifetime_init | ( | symbol_tablet & | symbol_table, |
const source_locationt & | source_location, | ||
message_handlert & | message_handler | ||
) |
Definition at line 27 of file static_lifetime_init.cpp.
References code_blockt::add(), exprt::add_source_location(), CPROVER_PREFIX, namespace_baset::follow(), forall_symbols, from_integer(), code_function_callt::function(), 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(), exprt::move_to_operands(), symbolt::name, code_typet::return_type(), irept::set(), array_typet::size(), size_type(), symbolt::symbol_expr(), symbol_tablet::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().