CBMC
static_lifetime_init.h File Reference
+ Include dependency graph for static_lifetime_init.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define INITIALIZE_FUNCTION   CPROVER_PREFIX "initialize"
 

Functions

void static_lifetime_init (symbol_table_baset &symbol_table, const source_locationt &source_location)
 
void recreate_initialize_function (goto_modelt &, message_handlert &)
 Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto model that have static lifetime. More...
 

Macro Definition Documentation

◆ INITIALIZE_FUNCTION

#define INITIALIZE_FUNCTION   CPROVER_PREFIX "initialize"

Definition at line 24 of file static_lifetime_init.h.

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()

void static_lifetime_init ( symbol_table_baset symbol_table,
const source_locationt source_location 
)

Definition at line 99 of file static_lifetime_init.cpp.