cbmc/rebuild__goto__start__function_8h_source.html

/*******************************************************************\


Module: Goto Programs


Author: Thomas Kiley, thomas@diffblue.com


\*******************************************************************/


#ifndef CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H

#define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H


#include <memory>


#include <util/irep.h>


class languaget;

class message_handlert;

class optionst;

class symbol_table_baset;


void remove_existing_entry_point(symbol_table_baset &);


const irep_idt &get_entry_point_mode(const symbol_table_baset &);


std::unique_ptr<languaget> get_entry_point_language(

  const symbol_table_baset &symbol_table,

  const optionst &options,

  message_handlert &message_handler);


#endif // CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H

dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38

languaget
Definition language.h:37

message_handlert
Definition message.h:27

optionst
Definition options.h:23

symbol_table_baset
The symbol table base class interface.
Definition symbol_table_base.h:23

irep.h

remove_existing_entry_point
void remove_existing_entry_point(symbol_table_baset &)
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
Definition rebuild_goto_start_function.cpp:46

get_entry_point_mode
const irep_idt & get_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.
Definition rebuild_goto_start_function.cpp:39

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.
Definition rebuild_goto_start_function.cpp:24