Statement List Language Entry Point. More...
#include "statement_list_entry_point.h"#include <util/c_types.h>#include <util/config.h>#include <util/message.h>#include <util/pointer_expr.h>#include <util/std_code.h>#include <util/symbol_table_base.h>#include <goto-programs/adjust_float_expressions.h>#include <goto-programs/goto_functions.h>#include <linking/static_lifetime_init.h>
Include dependency graph for statement_list_entry_point.cpp:Go to the source code of this file.
Macros | |
| #define | DB_ENTRY_POINT_POSTFIX "_entry_point" |
| Postfix for the artificial data block that is created when calling a main symbol that is a function block. More... | |
| #define | CPROVER_HIDE CPROVER_PREFIX "HIDE" |
| Name of the CPROVER-specific hide label. More... | |
Functions | |
| static bool | is_main_symbol_invalid (const symbol_table_baset &symbol_table, message_handlert &message_handler, const irep_idt &main_symbol_name) |
| Searches for symbols with the given name (which is considered to be the name of the main symbol) and returns false if there is exactly one symbol with that name in the given symbol table. More... | |
| static void | add_initialize_call (code_blockt &function_body, const symbol_table_baset &symbol_table, const source_locationt &main_symbol_location) |
| Creates a call to __CPROVER_initialize and adds it to the start function's body. More... | |
| static void | add_main_function_block_call (code_blockt &function_body, symbol_table_baset &symbol_table, const symbolt &main_function_block) |
| Creates a call to the main function block and adds it to the start function's body. More... | |
| static void | generate_statement_list_init_function (symbol_table_baset &symbol_table) |
| Creates __CPROVER_initialize and adds it to the symbol table. More... | |
| static void | generate_rounding_mode (symbol_table_baset &symbol_table) |
| Creates __CPROVER_rounding_mode and adds it to the symbol table. More... | |
| bool | generate_statement_list_start_function (const symbolt &main, symbol_table_baset &symbol_table, message_handlert &message_handler) |
| Creates a start function and adds it to the symbol table. More... | |
| bool | statement_list_entry_point (symbol_table_baset &symbol_table, message_handlert &message_handler) |
| Creates a new entry point for the Statement List language. More... | |
Detailed Description
Statement List Language Entry Point.
Definition in file statement_list_entry_point.cpp.
Macro Definition Documentation
◆ CPROVER_HIDE
| #define CPROVER_HIDE CPROVER_PREFIX "HIDE" |
Name of the CPROVER-specific hide label.
Definition at line 31 of file statement_list_entry_point.cpp.
◆ DB_ENTRY_POINT_POSTFIX
| #define DB_ENTRY_POINT_POSTFIX "_entry_point" |
Postfix for the artificial data block that is created when calling a main symbol that is a function block.
Definition at line 28 of file statement_list_entry_point.cpp.
Function Documentation
◆ add_initialize_call()
|
static |
Creates a call to __CPROVER_initialize and adds it to the start function's body.
- Parameters
-
[out] function_body Body of the start function. symbol_table Symbol table, containing the symbol for __CPROVER_initialize. main_symbol_location Source location of the main symbol.
Definition at line 81 of file statement_list_entry_point.cpp.
◆ add_main_function_block_call()
|
static |
Creates a call to the main function block and adds it to the start function's body.
- Parameters
-
[out] function_body Body of the start function. symbol_table Symbol table, containing the main symbol. main_function_block Main symbol of this application.
Definition at line 97 of file statement_list_entry_point.cpp.
◆ generate_rounding_mode()
|
static |
Creates __CPROVER_rounding_mode and adds it to the symbol table.
- Parameters
-
[out] symbol_table Symbol table that should contain the symbol.
Definition at line 143 of file statement_list_entry_point.cpp.
◆ generate_statement_list_init_function()
|
static |
Creates __CPROVER_initialize and adds it to the symbol table.
- Parameters
-
[out] symbol_table Symbol table that should contain the function.
Definition at line 123 of file statement_list_entry_point.cpp.
◆ generate_statement_list_start_function()
| bool generate_statement_list_start_function | ( | const symbolt & | main, |
| symbol_table_baset & | symbol_table, | ||
| message_handlert & | message_handler | ||
| ) |
Creates a start function and adds it to the symbol table.
This start function contains calls to __CPROVER_initialize and the main symbol.
- Parameters
-
main Main symbol of this application. [out] symbol_table Symbol table that should contain the function. message_handler Handler that is responsible for error messages.
Definition at line 160 of file statement_list_entry_point.cpp.
◆ is_main_symbol_invalid()
|
static |
Searches for symbols with the given name (which is considered to be the name of the main symbol) and returns false if there is exactly one symbol with that name in the given symbol table.
Prints an error message and returns true if there are multiple or no matches.
- Parameters
-
symbol_table Symbol table to search through. message_handler Used for printing error messages. main_symbol_name Name of the symbol to look for.
- Returns
- False if there is exactly one match, true otherwise.
Definition at line 41 of file statement_list_entry_point.cpp.
◆ statement_list_entry_point()
| bool statement_list_entry_point | ( | symbol_table_baset & | symbol_table, |
| message_handlert & | message_handler | ||
| ) |
Creates a new entry point for the Statement List language.
- Parameters
-
[out] symbol_table Symbol table of the current TIA program. Gets filled with the symbols that are necessary for a proper entry point. message_handler Handler that is responsible for error messages.
Definition at line 191 of file statement_list_entry_point.cpp.
