initialize_goto_model.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Initialize a Goto Program
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/

 
#ifndef CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
#define CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
 
#include "goto_model.h"
 
class language_filest;
class message_handlert;
class optionst;
 
goto_modelt initialize_goto_model(
  const std::vector<std::string> &files,
  message_handlert &message_handler,
  const optionst &options);

void initialize_from_source_files(
  const std::list<std::string> &sources,
  const optionst &options,
  language_filest &language_files,
  symbol_tablet &symbol_table,
  message_handlert &message_handler);

void set_up_custom_entry_point(
  language_filest &language_files,
  symbol_tablet &symbol_table,
  const std::function<std::size_t(const irep_idt &)> &unload,
  const optionst &options,
  bool try_mode_lookup,
  message_handlert &message_handler);

void update_max_malloc_size(goto_modelt &, message_handlert &);
 
#endif // CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H