CBMC
static_lifetime_init.cpp File Reference
+ Include dependency graph for static_lifetime_init.cpp:

Go to the source code of this file.

Functions

static std::optional< codetstatic_lifetime_init (const irep_idt &identifier, symbol_table_baset &symbol_table)
 
void static_lifetime_init (symbol_table_baset &symbol_table, const source_locationt &source_location)
 
void recreate_initialize_function (goto_modelt &goto_model, message_handlert &message_handler)
 Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto model that have static lifetime. More...
 

Function Documentation

◆ recreate_initialize_function()

void recreate_initialize_function ( goto_modelt goto_model,
message_handlert message_handler 
)

Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto model that have static lifetime.

It is an error if CPROVER_INITIALIZE was not present beforehand.

Definition at line 165 of file static_lifetime_init.cpp.

◆ static_lifetime_init() [1/2]

static std::optional<codet> static_lifetime_init ( const irep_idt identifier,
symbol_table_baset symbol_table 
)
static

Definition at line 25 of file static_lifetime_init.cpp.

◆ static_lifetime_init() [2/2]

void static_lifetime_init ( symbol_table_baset symbol_table,
const source_locationt source_location 
)

Definition at line 99 of file static_lifetime_init.cpp.