CBMC
rebuild_goto_start_function.h File Reference

Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m. More...

#include <memory>
#include <util/irep.h>
+ Include dependency graph for rebuild_goto_start_function.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void remove_existing_entry_point (symbol_table_baset &)
 Eliminate the existing entry point function symbol and any symbols created in that scope from the symbol_table. More...
 
const irep_idtget_entry_point_mode (const symbol_table_baset &)
 Find out the mode of the current entry point to determine the mode of the replacement entry point. More...
 
std::unique_ptr< languagetget_entry_point_language (const symbol_table_baset &symbol_table, const optionst &options, message_handlert &message_handler)
 Find the language corresponding to the __CPROVER_start function. More...
 

Detailed Description

Goto Programs Author: Thomas Kiley, thoma.nosp@m.s@di.nosp@m.ffblu.nosp@m.e.co.nosp@m.m.

Definition in file rebuild_goto_start_function.h.

Function Documentation

◆ get_entry_point_language()

std::unique_ptr<languaget> get_entry_point_language ( const symbol_table_baset symbol_table,
const optionst options,
message_handlert message_handler 
)

Find the language corresponding to the __CPROVER_start function.

Parameters
symbol_tableThe symbol table of the goto model.
optionsCommand-line options
message_handlerThe message handler to report any messages with

Definition at line 24 of file rebuild_goto_start_function.cpp.

◆ get_entry_point_mode()

const irep_idt& get_entry_point_mode ( const symbol_table_baset symbol_table)

Find out the mode of the current entry point to determine the mode of the replacement entry point.

Returns
A mode string saying which language to use

Definition at line 39 of file rebuild_goto_start_function.cpp.

◆ remove_existing_entry_point()

void remove_existing_entry_point ( symbol_table_baset symbol_table)

Eliminate the existing entry point function symbol and any symbols created in that scope from the symbol_table.

Definition at line 46 of file rebuild_goto_start_function.cpp.