cprover
link_to_library.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Library Linking
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H
13
#define CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H
14
15
#include <functional>
16
#include <set>
17
18
#include <
util/deprecate.h
>
19
#include <
util/irep.h
>
20
21
class
goto_functionst
;
22
class
goto_modelt
;
23
class
message_handlert
;
24
class
symbol_tablet
;
25
26
DEPRECATED
(
SINCE
(2019, 2, 28,
"Use link_to_library(goto_model, ...) instead"
))
27
void
link_to_library
(
28
symbol_tablet
&,
29
goto_functionst
&,
30
message_handlert
&,
31
const std::function<
32
void
(const std::set<
irep_idt
> &,
symbol_tablet
&,
message_handlert
&)> &);
33
34
void
link_to_library
(
35
goto_modelt
&,
36
message_handlert
&,
37
const std::function<
38
void
(const std::set<
irep_idt
> &,
symbol_tablet
&,
message_handlert
&)> &);
39
40
#endif // CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
symbol_tablet
The symbol table.
Definition:
symbol_table.h:20
goto_modelt
Definition:
goto_model.h:26
deprecate.h
message_handlert
Definition:
message.h:28
SINCE
#define SINCE(year, month, day, msg)
Definition:
deprecate.h:26
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:23
DEPRECATED
#define DEPRECATED(msg)
Definition:
deprecate.h:23
link_to_library
void link_to_library(symbol_tablet &, goto_functionst &, message_handlert &, const std::function< void(const std::set< irep_idt > &, symbol_tablet &, message_handlert &)> &)
Complete missing function definitions using the library.
Definition:
link_to_library.cpp:98
irep.h
goto-programs
link_to_library.h
Generated by
1.8.20