|
CBMC
|
#include "ansi_c_entry_point.h"#include <util/arith_tools.h>#include <util/c_types.h>#include <util/config.h>#include <util/message.h>#include <util/pointer_expr.h>#include <util/range.h>#include <util/symbol_table.h>#include <goto-programs/goto_functions.h>#include <linking/static_lifetime_init.h>#include "c_nondet_symbol_factory.h"#include "expr2c.h"
Include dependency graph for ansi_c_entry_point.cpp:Go to the source code of this file.
Functions | |
| exprt::operandst | build_function_environment (const code_typet::parameterst ¶meters, code_blockt &init_code, symbol_tablet &symbol_table, const c_object_factory_parameterst &object_factory_parameters) |
| void | record_function_outputs (const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table) |
| bool | ansi_c_entry_point (symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters) |
| bool | generate_ansi_c_start_function (const symbolt &symbol, symbol_tablet &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters) |
| Generate a _start function for a specific function. More... | |
| bool ansi_c_entry_point | ( | symbol_tablet & | symbol_table, |
| message_handlert & | message_handler, | ||
| const c_object_factory_parameterst & | object_factory_parameters | ||
| ) |
Definition at line 106 of file ansi_c_entry_point.cpp.
| exprt::operandst build_function_environment | ( | const code_typet::parameterst & | parameters, |
| code_blockt & | init_code, | ||
| symbol_tablet & | symbol_table, | ||
| const c_object_factory_parameterst & | object_factory_parameters | ||
| ) |
Definition at line 26 of file ansi_c_entry_point.cpp.
| bool generate_ansi_c_start_function | ( | const symbolt & | symbol, |
| symbol_tablet & | symbol_table, | ||
| message_handlert & | message_handler, | ||
| const c_object_factory_parameterst & | object_factory_parameters | ||
| ) |
Generate a _start function for a specific function.
| symbol | The symbol for the function that should be used as the entry point |
| symbol_table | The symbol table for the program. The new _start function symbol will be added to this table |
| message_handler | The message handler |
| object_factory_parameters | configuration parameters for the object factory |
Definition at line 191 of file ansi_c_entry_point.cpp.
| void record_function_outputs | ( | const symbolt & | function, |
| code_blockt & | init_code, | ||
| symbol_tablet & | symbol_table | ||
| ) |
Definition at line 56 of file ansi_c_entry_point.cpp.