cprover
goto_function.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: A GOTO Function
4 
5 Author: Daniel Kroening
6 
7 Date: May 2018
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
15 #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
16 
17 #include <iosfwd>
18 
19 #include <util/find_symbols.h>
20 #include <util/std_types.h>
21 
22 #include "goto_program.h"
23 
27 {
28 public:
30 
31  typedef std::vector<irep_idt> parameter_identifierst;
37 
38  bool body_available() const
39  {
40  return !body.instructions.empty();
41  }
42 
43  void set_parameter_identifiers(const code_typet &code_type)
44  {
45  parameter_identifiers.clear();
46  parameter_identifiers.reserve(code_type.parameters().size());
47  for(const auto &parameter : code_type.parameters())
48  parameter_identifiers.push_back(parameter.get_identifier());
49  }
50 
51  bool is_hidden() const
52  {
53  return function_is_hidden;
54  }
55 
56  void make_hidden()
57  {
58  function_is_hidden = true;
59  }
60 
62  {
63  }
64 
65  void clear()
66  {
67  body.clear();
68  parameter_identifiers.clear();
69  function_is_hidden = false;
70  }
71 
72  void swap(goto_functiont &other)
73  {
74  body.swap(other.body);
76  std::swap(function_is_hidden, other.function_is_hidden);
77  }
78 
79  void copy_from(const goto_functiont &other)
80  {
81  body.copy_from(other.body);
84  }
85 
86  goto_functiont(const goto_functiont &) = delete;
88 
90  : body(std::move(other.body)),
93  {
94  }
95 
97  {
98  body = std::move(other.body);
99  parameter_identifiers = std::move(other.parameter_identifiers);
100  function_is_hidden = other.function_is_hidden;
101  return *this;
102  }
103 
108  void validate(const namespacet &ns, const validation_modet vm) const;
109 
110 protected:
112 };
113 
114 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);
115 
116 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
Base type of functions.
Definition: std_types.h:744
const parameterst & parameters() const
Definition: std_types.h:860
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
goto_functiont & operator=(const goto_functiont &)=delete
goto_programt body
Definition: goto_function.h:29
bool is_hidden() const
Definition: goto_function.h:51
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:31
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:36
void copy_from(const goto_functiont &other)
Definition: goto_function.h:79
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
goto_functiont(goto_functiont &&other)
Definition: goto_function.h:89
void make_hidden()
Definition: goto_function.h:56
bool body_available() const
Definition: goto_function.h:38
void swap(goto_functiont &other)
Definition: goto_function.h:72
goto_functiont(const goto_functiont &)=delete
goto_functiont & operator=(goto_functiont &&other)
Definition: goto_function.h:96
void set_parameter_identifiers(const code_typet &code_type)
Definition: goto_function.h:43
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
Definition: goto_program.h:754
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:748
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
void get_local_identifiers(const goto_functiont &, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
Concrete Goto Program.
Pre-defined types.
validation_modet