CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
link_goto_model.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Read Goto Programs
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
13#define CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
14
15#include <util/replace_symbol.h>
16
17class goto_modelt;
18class message_handlert;
19
25[[nodiscard]] std::optional<replace_symbolt::expr_mapt>
26link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &);
27
30void finalize_linking(
31 goto_modelt &dest,
32 const replace_symbolt::expr_mapt &type_updates);
33
34#endif // CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
goto_modelt
Definition goto_model.h:27
message_handlert
Definition message.h:27
replace_symbolt::expr_mapt
std::unordered_map< irep_idt, exprt > expr_mapt
Definition replace_symbol.h:30
finalize_linking
void finalize_linking(goto_modelt &dest, const replace_symbolt::expr_mapt &type_updates)
Apply type_updates to dest, where type_updates were constructed from one or more calls to link_goto_m...
Definition link_goto_model.cpp:164
link_goto_model
std::optional< replace_symbolt::expr_mapt > link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &)
Link goto model src into goto model dest, invalidating src in this process.
Definition link_goto_model.cpp:125
replace_symbol.h