link_goto_model.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Read Goto Programs
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
#define CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
 
#include <util/nodiscard.h>
#include <util/replace_symbol.h>
 
class goto_modelt;
class message_handlert;
 
NODISCARD optionalt<replace_symbolt::expr_mapt>
link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &);
 
void finalize_linking(
  goto_modelt &dest,
  const replace_symbolt::expr_mapt &type_updates);
 
#endif // CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H