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 
33 
34  typedef std::vector<irep_idt> parameter_identifierst;
35 
43 
44  bool body_available() const
45  {
46  return !body.instructions.empty();
47  }
48 
49  bool is_inlined() const
50  {
51  return type.get_bool(ID_C_inlined);
52  }
53 
54  bool is_hidden() const
55  {
56  return type.get_bool(ID_C_hide);
57  }
58 
59  void make_hidden()
60  {
61  type.set(ID_C_hide, true);
62  }
63 
65  {
66  }
67 
68  void clear()
69  {
70  body.clear();
71  type.clear();
72  parameter_identifiers.clear();
73  }
74 
78  void update_instructions_function(const irep_idt &function_id)
79  {
81  }
82 
83  void swap(goto_functiont &other)
84  {
85  body.swap(other.body);
86  type.swap(other.type);
88  }
89 
90  void copy_from(const goto_functiont &other)
91  {
92  body.copy_from(other.body);
93  type = other.type;
95  }
96 
97  goto_functiont(const goto_functiont &) = delete;
98  goto_functiont &operator=(const goto_functiont &) = delete;
99 
101  : body(std::move(other.body)),
102  type(std::move(other.type)),
104  {
105  }
106 
108  {
109  body = std::move(other.body);
110  type = std::move(other.type);
111  parameter_identifiers = std::move(other.parameter_identifiers);
112  return *this;
113  }
114 
119  void validate(const namespacet &ns, const validation_modet vm) const
120  {
121  body.validate(ns, vm);
122 
123  find_symbols_sett typetags;
124  find_type_symbols(type, typetags);
125  const symbolt *symbol;
126  for(const auto &identifier : typetags)
127  {
128  DATA_CHECK(
129  vm,
130  !ns.lookup(identifier, symbol),
131  id2string(identifier) + " not found");
132  }
133 
134  validate_full_type(type, ns, vm);
135  }
136 };
137 
138 void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);
139 
140 #endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
Base type of functions.
Definition: std_types.h:751
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void swap(goto_functiont &other)
Definition: goto_function.h:83
void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed (full check, including checks of subtypes)
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:42
goto_programt body
Definition: goto_function.h:29
void make_hidden()
Definition: goto_function.h:59
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
Symbol table entry.
Definition: symbol.h:27
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
std::vector< irep_idt > parameter_identifierst
Definition: goto_function.h:34
void update_instructions_function(const irep_idt &function_id)
update the function member in each instruction
Definition: goto_function.h:78
goto_functiont & operator=(const goto_functiont &)=delete
void clear()
Clear the goto program.
Definition: goto_program.h:647
goto_functiont(goto_functiont &&other)
bool is_inlined() const
Definition: goto_function.h:49
The empty type.
Definition: std_types.h:48
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
Definition: goto_program.h:693
void copy_from(const goto_functiont &other)
Definition: goto_function.h:90
code_typet type
The type of the function, indicating the return type and parameter types.
Definition: goto_function.h:32
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
goto_functiont & operator=(goto_functiont &&other)
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:641
bool is_hidden() const
Definition: goto_function.h:54
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
Pre-defined types.
bool body_available() const
Definition: goto_function.h:44
void update_instructions_function(const irep_idt &function_id)
Sets the function member of each instruction if not yet set Note that a goto program need not be a go...
Definition: goto_program.h:594
void clear()
Definition: irep.h:313
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
void swap(irept &irep)
Definition: irep.h:303
validation_modet
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...
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
Concrete Goto Program.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286