cprover
goto_model.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbol Table + CFG
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
14 
15 #include <util/symbol_table.h>
16 
17 #include "goto_functions.h"
18 
19 // A model is a pair consisting of a symbol table
20 // and the CFGs for the functions.
21 
23 {
24 public:
27 
28  void clear()
29  {
32  }
33 
34  void output(std::ostream &out)
35  {
37  goto_functions.output(ns, out);
38  }
39 
41  {
42  }
43 
44  // Copying is normally too expensive
45  goto_modelt(const goto_modelt &)=delete;
46  goto_modelt &operator=(const goto_modelt &)=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  symbol_table(std::move(other.symbol_table)),
56  goto_functions(std::move(other.goto_functions))
57  {
58  }
59 
61  {
62  symbol_table=std::move(other.symbol_table);
63  goto_functions=std::move(other.goto_functions);
64  return *this;
65  }
66 };
67 
68 #endif // CPROVER_GOTO_PROGRAMS_GOTO_MODEL_H
void output(std::ostream &out)
Definition: goto_model.h:34
Goto Programs with Functions.
STL namespace.
symbol_tablet symbol_table
Definition: goto_model.h:25
goto_modelt & operator=(goto_modelt &&other)
Definition: goto_model.h:60
void output(const namespacet &ns, std::ostream &out) const
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Symbol table.
goto_modelt & operator=(const goto_modelt &)=delete
void clear()
Definition: goto_model.h:28
goto_functionst goto_functions
Definition: goto_model.h:26
goto_modelt(goto_modelt &&other)
Definition: goto_model.h:54