cprover
goto_inline.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Function Inlining
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
13
14#ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H
15#define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H
16
17#include <util/json.h>
18
19class goto_functionst;
20class goto_modelt;
22class namespacet;
23
24// do a full inlining
25
26void goto_inline(
27 goto_modelt &goto_model,
28 message_handlert &message_handler,
29 bool adjust_function=false);
30
31void goto_inline(
32 goto_functionst &goto_functions,
33 const namespacet &ns,
34 message_handlert &message_handler,
35 bool adjust_function=false);
36
37// inline those functions marked as "inlined" and functions with less
38// than _smallfunc_limit instructions
39
41 goto_modelt &goto_model,
42 message_handlert &message_handler,
43 unsigned smallfunc_limit=0,
44 bool adjust_function=false);
45
47 goto_functionst &goto_functions,
48 const namespacet &ns,
49 message_handlert &message_handler,
50 unsigned smallfunc_limit=0,
51 bool adjust_function=false);
52
53// transitively inline all calls the given function makes
54
56 goto_modelt &goto_model,
57 const irep_idt function,
58 message_handlert &message_handler,
59 bool adjust_function=false,
60 bool caching=true);
61
63 goto_functionst &goto_functions,
64 const irep_idt function,
65 const namespacet &ns,
66 message_handlert &message_handler,
67 bool adjust_function=false,
68 bool caching=true);
69
72 const irep_idt function,
73 message_handlert &message_handler,
74 bool adjust_function=false,
75 bool caching=true);
76
77#endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A collection of goto functions.
Definition: json.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function=false)
Inline every function call into the entry_point() function.
Definition: goto_inline.cpp:26
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function=false, bool caching=true)
Transitively inline all function calls made from a particular function.
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit=0, bool adjust_function=false)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
jsont goto_function_inline_and_log(goto_modelt &, const irep_idt function, message_handlert &message_handler, bool adjust_function=false, bool caching=true)