cprover
|
#include "static_lifetime_init.h"
#include <cassert>
#include <cstdlib>
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/expr_initializer.h>
#include <util/namespace.h>
#include <util/prefix.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include <goto-programs/goto_functions.h>
Go to the source code of this file.
Functions | |
bool | static_lifetime_init (symbol_tablet &symbol_table, const source_locationt &source_location, message_handlert &message_handler) |
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().