cprover
goto_functions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Programs with Functions
4 
5 Author: Daniel Kroening
6 
7 Date: June 2003
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
15 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
16 
17 #include "goto_function.h"
18 
19 #include <util/cprover_prefix.h>
20 
23 {
24 public:
26  typedef std::map<irep_idt, goto_functiont> function_mapt;
28 
29 private:
36 
37 public:
40  {
41  }
42 
43  // Copying is unavailable as base class copy is deleted
44  // MSVC is unable to automatically determine this
45  goto_functionst(const goto_functionst &)=delete;
46  goto_functionst &operator=(const goto_functionst &)=delete;
47 
48  // Move operations need to be explicitly enabled as they are deleted with the
49  // copy operations
50  // default for move operations isn't available on Windows yet, so define
51  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
52  // under "Defaulted and Deleted Functions")
53 
55  function_map(std::move(other.function_map)),
57  {
58  }
59 
61  {
62  function_map=std::move(other.function_map);
63  unused_location_number=other.unused_location_number;
64  return *this;
65  }
66 
68  void unload(const irep_idt &name) { function_map.erase(name); }
69 
70  void clear()
71  {
72  function_map.clear();
73  }
74 
77  void compute_loop_numbers();
80 
84  {
85  for(auto &func : function_map)
86  {
87  func.second.update_instructions_function(func.first);
88  }
89  }
90 
91  void update()
92  {
98  }
99 
101  static inline irep_idt entry_point()
102  {
103  // do not confuse with C's "int main()"
104  return CPROVER_PREFIX "_start";
105  }
106 
107  void swap(goto_functionst &other)
108  {
109  function_map.swap(other.function_map);
110  }
111 
112  void copy_from(const goto_functionst &other)
113  {
114  for(const auto &fun : other.function_map)
115  function_map[fun.first].copy_from(fun.second);
116  }
117 
118  std::vector<function_mapt::const_iterator> sorted() const;
119  std::vector<function_mapt::iterator> sorted();
120 
125  void validate(const namespacet &ns, const validation_modet vm) const
126  {
127  for(const auto &entry : function_map)
128  {
129  const goto_functiont &goto_function = entry.second;
130  const auto &function_name = entry.first;
131 
132  DATA_CHECK(
133  vm,
134  goto_function.type == ns.lookup(function_name).type,
135  id2string(function_name) + " type inconsistency\ngoto program type: " +
136  goto_function.type.id_string() +
137  "\nsymbol table type: " + ns.lookup(function_name).type.id_string());
138 
139  goto_function.validate(ns, vm);
140  }
141  }
142 };
143 
144 #define Forall_goto_functions(it, functions) \
145  for(goto_functionst::function_mapt::iterator \
146  it=(functions).function_map.begin(); \
147  it!=(functions).function_map.end(); it++)
148 
149 #define forall_goto_functions(it, functions) \
150  for(goto_functionst::function_mapt::const_iterator \
151  it=(functions).function_map.begin(); \
152  it!=(functions).function_map.end(); it++)
153 
154 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
goto_functionst::sorted
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
Definition: goto_functions.cpp:62
goto_functiont::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
Definition: goto_function.h:119
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
goto_functionst::clear
void clear()
Definition: goto_functions.h:70
goto_functionst::compute_target_numbers
void compute_target_numbers()
Definition: goto_functions.cpp:44
goto_functionst::update_instructions_function
void update_instructions_function()
update the function member in each instruction by setting it to the goto function's identifier
Definition: goto_functions.h:83
goto_functionst::function_mapt
std::map< irep_idt, goto_functiont > function_mapt
Definition: goto_functions.h:26
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_functionst::goto_functionst
goto_functionst(goto_functionst &&other)
Definition: goto_functions.h:54
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
validation_modet
validation_modet
Definition: validation_mode.h:12
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
goto_functionst::compute_loop_numbers
void compute_loop_numbers()
Definition: goto_functions.cpp:52
cprover_prefix.h
goto_functionst::operator=
goto_functionst & operator=(const goto_functionst &)=delete
goto_functionst::unload
void unload(const irep_idt &name)
Remove function from the function map.
Definition: goto_functions.h:68
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_functionst::goto_functionst
goto_functionst()
Definition: goto_functions.h:38
goto_functionst::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto functions are well-formed.
Definition: goto_functions.h:125
goto_functionst::copy_from
void copy_from(const goto_functionst &other)
Definition: goto_functions.h:112
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functionst::update
void update()
Definition: goto_functions.h:91
goto_functionst::swap
void swap(goto_functionst &other)
Definition: goto_functions.h:107
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
goto_functiont::type
code_typet type
The type of the function, indicating the return type and parameter types.
Definition: goto_function.h:32
goto_function.h
goto_functionst::compute_incoming_edges
void compute_incoming_edges()
Definition: goto_functions.cpp:36
goto_functionst::operator=
goto_functionst & operator=(goto_functionst &&other)
Definition: goto_functions.h:60
goto_functionst::unused_location_number
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...
Definition: goto_functions.h:35