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
goto_functiont::body
goto_programt body
Definition: goto_function.h:29
goto_functiont::function_is_hidden
bool function_is_hidden
Definition: goto_function.h:111
goto_functiont::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
Definition: goto_function.cpp:36
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:625
goto_functiont::goto_functiont
goto_functiont(goto_functiont &&other)
Definition: goto_function.h:89
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_functiont::body_available
bool body_available() const
Definition: goto_function.h:38
get_local_identifiers
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...
Definition: goto_function.cpp:18
goto_functiont::swap
void swap(goto_functiont &other)
Definition: goto_function.h:72
find_symbols.h
goto_functiont::operator=
goto_functiont & operator=(const goto_functiont &)=delete
std_types.h
Pre-defined types.
code_typet
Base type of functions.
Definition: std_types.h:744
validation_modet
validation_modet
Definition: validation_mode.h:13
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
goto_functiont::is_hidden
bool is_hidden() const
Definition: goto_function.h:51
goto_functiont::set_parameter_identifiers
void set_parameter_identifiers(const code_typet &code_type)
Definition: goto_function.h:43
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:754
goto_program.h
Concrete Goto Program.
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
goto_functiont::operator=
goto_functiont & operator=(goto_functiont &&other)
Definition: goto_function.h:96
goto_functiont::goto_functiont
goto_functiont(const goto_functiont &)=delete
goto_functiont::clear
void clear()
Definition: goto_function.h:65
goto_functiont::copy_from
void copy_from(const goto_functiont &other)
Definition: goto_function.h:79
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
goto_functiont::parameter_identifierst
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:31
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:36
goto_functiont::make_hidden
void make_hidden()
Definition: goto_function.h:56
goto_programt::swap
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:748
goto_functiont::goto_functiont
goto_functiont()
Definition: goto_function.h:61