Go to the documentation of this file.
21 #define INITIALIZE_FUNCTION CPROVER_PREFIX "initialize"
24 #define ROUNDING_MODE_NAME CPROVER_PREFIX "rounding_mode"
28 #define DB_ENTRY_POINT_POSTFIX "_entry_point"
31 #define CPROVER_HIDE CPROVER_PREFIX "HIDE"
48 for(
const std::pair<const irep_idt, symbolt> &pair : symbol_table)
50 if(pair.first == main_symbol_name && pair.second.type.id() == ID_code)
55 message.error() <<
"main symbol `" << main_symbol_name
69 message.error() <<
"main symbol `" << main_symbol_name <<
"' not found"
89 function_body.
add(call_init);
100 const symbolt &main_function_block)
107 instance_data_block.
name =
111 instance_data_block.
mode = ID_statement_list;
112 symbol_table.
add(instance_data_block);
118 function_body.
add(call_main);
127 init.
mode = ID_statement_list;
133 for(
const std::pair<const irep_idt, symbolt> &pair : symbol_table)
135 const symbolt &symbol = pair.second;
137 dest.add(
code_assignt{pair.second.symbol_expr(), pair.second.value});
139 init.
value = std::move(dest);
140 symbol_table.add(init);
155 rounding_mode.
value = rounding_val;
156 symbol_table.
add(rounding_mode);
183 start_symbol.
value.
swap(start_function_body);
186 if(!symbol_table.
insert(std::move(start_symbol)).second)
212 symbol_table, message_handler,
config.
main.value()))
222 symbol_table, message_handler, ID_statement_list_main_function))
224 main_symbol_name = ID_statement_list_main_function;
230 if(
main.value.is_nil())
241 main, symbol_table, message_handler);
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
bool generate_statement_list_start_function(const symbolt &main, symbol_tablet &symbol_table, message_handlert &message_handler)
Creates a start function and adds it to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & subtype() const
Statement List Language Type Checking.
static void add_main_function_block_call(code_blockt &function_body, symbol_tablet &symbol_table, const symbolt &main_function_block)
Creates a call to the main function block and adds it to the start function's body.
typet type
Type of symbol.
optionalt< std::string > main
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
#define INITIALIZE_FUNCTION
Name of the CPROVER-specific function that initializes static variables.
static void generate_rounding_mode(symbol_tablet &symbol_table)
Creates __CPROVER_rounding_mode and adds it to the symbol table.
static void add_initialize_call(code_blockt &function_body, const symbol_tablet &symbol_table, const source_locationt &main_symbol_location)
Creates a call to __CPROVER_initialize and adds it to the start function's body.
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
typet & type()
Return the type of the expression.
codet representation of a function call statement.
static bool is_main_symbol_invalid(const symbol_tablet &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 ...
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
irep_idt mode
Language mode.
const irep_idt & get_base_name() const
signedbv_typet signed_int_type()
const std::string & id2string(const irep_idt &d)
static void generate_statement_list_init_function(symbol_tablet &symbol_table)
Creates __CPROVER_initialize and adds it to the symbol table.
codet representation of a label for branch targets.
#define PRECONDITION(CONDITION)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Statement List Language Entry Point.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
exprt::operandst argumentst
void add(const codet &code)
const parameterst & parameters() const
int main(int argc, char *argv[])
#define DB_ENTRY_POINT_POSTFIX
Postfix for the artificial data block that is created when calling a main symbol that is a function b...
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
exprt value
Initial value of symbol.
A codet representing a skip statement.
source_locationt location
Source code location of definition of symbol.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool statement_list_entry_point(symbol_tablet &symbol_table, message_handlert &message_handler)
Creates a new entry point for the Statement List language.
Goto Programs with Functions.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Operator to return the address of an object.
#define CPROVER_HIDE
Name of the CPROVER-specific hide label.
source_locationt & add_source_location()
A codet representing an assignment in the program.
A constant literal expression.
#define ROUNDING_MODE_NAME
Name of the CPROVER-specific variable that specifies the rounding mode.
irep_idt name
The unique identifier.