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/deprecate.h>
20 #include <util/find_symbols.h>
21 #include <util/std_types.h>
22 
23 #include "goto_program.h"
24 
28 {
29 public:
31 
33  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
35 
36  typedef std::vector<irep_idt> parameter_identifierst;
37 
43 
44  bool body_available() const
45  {
46  return !body.instructions.empty();
47  }
48 
49  void set_parameter_identifiers(const code_typet &code_type)
50  {
51  parameter_identifiers.clear();
52  parameter_identifiers.reserve(code_type.parameters().size());
53  for(const auto &parameter : code_type.parameters())
54  parameter_identifiers.push_back(parameter.get_identifier());
55  }
56 
57  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
58  bool is_inlined() const
59  {
60  return type.get_bool(ID_C_inlined);
61  }
62 
63  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
64  bool is_hidden() const
65  {
66  return type.get_bool(ID_C_hide);
67  }
68 
69  DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead"))
70  void make_hidden()
71  {
72  type.set(ID_C_hide, true);
73  }
74 
76  {
77  }
78 
79  void clear()
80  {
81  body.clear();
82  type.clear();
83  parameter_identifiers.clear();
84  }
85 
86  void swap(goto_functiont &other)
87  {
88  body.swap(other.body);
89  type.swap(other.type);
91  }
92 
93  void copy_from(const goto_functiont &other)
94  {
95  body.copy_from(other.body);
96  type = other.type;
98  }
99 
100  goto_functiont(const goto_functiont &) = delete;
102 
104  : body(std::move(other.body)),
105  type(std::move(other.type)),
107  {
108  }
109 
111  {
112  body = std::move(other.body);
113  type = std::move(other.type);
114  parameter_identifiers = std::move(other.parameter_identifiers);
115  return *this;
116  }
117 
122  void validate(const namespacet &ns, const validation_modet vm) const;
123 };
124 
125 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);
126 
127 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
irept::clear
void clear()
Definition: irep.h:473
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:626
goto_functiont::goto_functiont
goto_functiont(goto_functiont &&other)
Definition: goto_function.h:103
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
goto_functiont::body_available
bool body_available() const
Definition: goto_function.h:44
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:86
find_symbols.h
empty_typet
The empty type.
Definition: std_types.h:46
deprecate.h
goto_functiont::operator=
goto_functiont & operator=(const goto_functiont &)=delete
std_types.h
Pre-defined types.
irept::swap
void swap(irept &irep)
Definition: irep.h:463
code_typet
Base type of functions.
Definition: std_types.h:736
validation_modet
validation_modet
Definition: validation_mode.h:13
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
goto_functiont::is_hidden
bool is_hidden() const
Definition: goto_function.h:64
goto_functiont::set_parameter_identifiers
void set_parameter_identifiers(const code_typet &code_type)
Definition: goto_function.h:49
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:783
goto_program.h
Concrete Goto Program.
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functiont::operator=
goto_functiont & operator=(goto_functiont &&other)
Definition: goto_function.h:110
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
goto_functiont::goto_functiont
goto_functiont(const goto_functiont &)=delete
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
goto_functiont::clear
void clear()
Definition: goto_function.h:79
goto_functiont::copy_from
void copy_from(const goto_functiont &other)
Definition: goto_function.h:93
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_functiont::is_inlined
bool is_inlined() const
Definition: goto_function.h:58
goto_functiont::parameter_identifierst
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:36
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:42
goto_functiont::make_hidden
void make_hidden()
Definition: goto_function.h:70
goto_functiont::type
code_typet type
The type of the function, indicating the return type and parameter types.
Definition: goto_function.h:34
goto_programt::swap
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:777
goto_functiont::goto_functiont
goto_functiont()
Definition: goto_function.h:75