CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
goto_function.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: A GOTO Function
4
5Author: Daniel Kroening
6
7Date: 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{
25public:
27
28 typedef std::vector<irep_idt> parameter_identifierst;
34
35 bool body_available() const
36 {
37 return !body.instructions.empty();
38 }
39
41 {
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
54 {
55 function_is_hidden = true;
56 }
57
61
62 void clear()
63 {
64 body.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
82
83 goto_functiont(const goto_functiont &) = delete;
85
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
107protected:
109};
110
111void get_local_identifiers(const goto_functiont &, std::set<irep_idt> &dest);
112
113#endif // CPROVER_GOTO_PROGRAMS_GOTO_FUNCTION_H
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base type of functions.
Definition std_types.h:583
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_functiont & operator=(goto_functiont &&other)
goto_programt body
bool is_hidden() const
goto_functiont & operator=(const goto_functiont &)=delete
std::vector< irep_idt > parameter_identifierst
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
void copy_from(const goto_functiont &other)
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
goto_functiont(goto_functiont &&other)
bool body_available() const
void swap(goto_functiont &other)
goto_functiont(const goto_functiont &)=delete
void set_parameter_identifiers(const code_typet &code_type)
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void clear()
Clear the goto program.
void swap(goto_programt &program)
Swap the goto program.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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.
STL namespace.
Pre-defined types.
validation_modet