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;
84  goto_functiont &operator=(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
goto_functiont::body
goto_programt body
Definition: goto_function.h:26
goto_functiont::function_is_hidden
bool function_is_hidden
Definition: goto_function.h:108
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:38
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:699
goto_functiont::goto_functiont
goto_functiont(goto_functiont &&other)
Definition: goto_function.h:86
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
goto_functiont::body_available
bool body_available() const
Definition: goto_function.h:35
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:20
goto_functiont::swap
void swap(goto_functiont &other)
Definition: goto_function.h:69
goto_functiont::operator=
goto_functiont & operator=(const goto_functiont &)=delete
std_types.h
code_typet
Base type of functions.
Definition: std_types.h:538
validation_modet
validation_modet
Definition: validation_mode.h:12
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:23
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
goto_functiont::is_hidden
bool is_hidden() const
Definition: goto_function.h:48
goto_functiont::set_parameter_identifiers
void set_parameter_identifiers(const code_typet &code_type)
Definition: goto_function.h:40
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:811
goto_program.h
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:592
goto_functiont::operator=
goto_functiont & operator=(goto_functiont &&other)
Definition: goto_function.h:93
goto_functiont::clear
void clear()
Definition: goto_function.h:62
goto_functiont::copy_from
void copy_from(const goto_functiont &other)
Definition: goto_function.h:76
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_functiont::parameter_identifierst
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:28
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:33
goto_functiont::make_hidden
void make_hidden()
Definition: goto_function.h:53
goto_programt::swap
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:805
goto_functiont::goto_functiont
goto_functiont()
Definition: goto_function.h:58