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_program.h"
19 
20 class goto_functionst:public goto_functions_templatet<goto_programt>
21 {
22 public:
23  goto_functionst()=default;
24 
25  // Copying is unavailable as base class copy is deleted
26  // MSVC is unable to automatically determine this
27  goto_functionst(const goto_functionst &)=delete;
28  goto_functionst &operator=(const goto_functionst &)=delete;
29 
30  // Move operations need to be explicitly enabled as they are deleted with the
31  // copy operations
32  // default for move operations isn't available on Windows yet, so define
33  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
34  // under "Defaulted and Deleted Functions")
35 
37  goto_functions_templatet(std::move(other))
38  {
39  }
40 
42  {
43  goto_functions_templatet::operator=(std::move(other));
44  return *this;
45  }
46 };
47 
48 #define Forall_goto_functions(it, functions) \
49  for(goto_functionst::function_mapt::iterator \
50  it=(functions).function_map.begin(); \
51  it!=(functions).function_map.end(); it++)
52 
53 #define forall_goto_functions(it, functions) \
54  for(goto_functionst::function_mapt::const_iterator \
55  it=(functions).function_map.begin(); \
56  it!=(functions).function_map.end(); it++)
57 
59  const goto_function_templatet<goto_programt> &goto_function,
60  std::set<irep_idt> &dest);
61 
62 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H
goto_functionst(goto_functionst &&other)
void get_local_identifiers(const goto_function_templatet< goto_programt > &goto_function, std::set< irep_idt > &dest)
STL namespace.
goto_functionst & operator=(goto_functionst &&other)
goto_functionst()=default
Goto Programs with Functions.
goto_functionst & operator=(const goto_functionst &)=delete
goto_functions_templatet & operator=(const goto_functions_templatet &)=delete
Concrete Goto Program.