CBMC
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 <util/std_types.h>
18 
19 #include "goto_program.h"
20 
24 {
25 public:
27 
28  typedef std::vector<irep_idt> parameter_identifierst;
34 
35  bool body_available() const
36  {
37  return !body.instructions.empty();
38  }
39 
40  void set_parameter_identifiers(const code_typet &code_type)
41  {
42  parameter_identifiers.clear();
43  parameter_identifiers.reserve(code_type.parameters().size());
44  for(const auto &parameter : code_type.parameters())
45  parameter_identifiers.push_back(parameter.get_identifier());
46  }
47 
48  bool is_hidden() const
49  {
50  return function_is_hidden;
51  }
52 
53  void make_hidden()
54  {
55  function_is_hidden = true;
56  }
57 
59  {
60  }
61 
62  void clear()
63  {
64  body.clear();
65  parameter_identifiers.clear();
66  function_is_hidden = false;
67  }
68 
69  void swap(goto_functiont &other)
70  {
71  body.swap(other.body);
73  std::swap(function_is_hidden, other.function_is_hidden);
74  }
75 
76  void copy_from(const goto_functiont &other)
77  {
78  body.copy_from(other.body);
81  }
82 
83  goto_functiont(const goto_functiont &) = delete;
85 
87  : body(std::move(other.body)),
90  {
91  }
92 
94  {
95  body = std::move(other.body);
96  parameter_identifiers = std::move(other.parameter_identifiers);
97  function_is_hidden = other.function_is_hidden;
98  return *this;
99  }
100 
105  void validate(const namespacet &ns, const validation_modet vm) const;
106 
107 protected:
109 };
110 
111 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);
112 
113 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
Base type of functions.
Definition: std_types.h:583
const parameterst & parameters() const
Definition: std_types.h:699
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_functiont & operator=(const goto_functiont &)=delete
goto_programt body
Definition: goto_function.h:26
bool is_hidden() const
Definition: goto_function.h:48
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:28
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:33
void copy_from(const goto_functiont &other)
Definition: goto_function.h:76
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:86
void make_hidden()
Definition: goto_function.h:53
bool body_available() const
Definition: goto_function.h:35
void swap(goto_functiont &other)
Definition: goto_function.h:69
goto_functiont(const goto_functiont &)=delete
goto_functiont & operator=(goto_functiont &&other)
Definition: goto_function.h:93
void set_parameter_identifiers(const code_typet &code_type)
Definition: goto_function.h:40
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
Definition: goto_program.h:820
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:814
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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