cprover
Loading...
Searching...
No Matches
std_code.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Data structures representing statements in a program
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "std_code.h"
13
14#include "arith_tools.h"
15#include "c_types.h"
16#include "pointer_expr.h"
17#include "string_constant.h"
18
22{
23 const irep_idt &statement=get_statement();
24
25 if(has_operands())
26 {
27 if(statement==ID_block)
28 return to_code(op0()).first_statement();
29 else if(statement==ID_label)
30 return to_code(op0()).first_statement();
31 }
32
33 return *this;
34}
35
39{
40 const irep_idt &statement=get_statement();
41
42 if(has_operands())
43 {
44 if(statement==ID_block)
45 return to_code(op0()).first_statement();
46 else if(statement==ID_label)
47 return to_code(op0()).first_statement();
48 }
49
50 return *this;
51}
52
56{
57 const irep_idt &statement=get_statement();
58
59 if(has_operands())
60 {
61 if(statement==ID_block)
62 return to_code(operands().back()).last_statement();
63 else if(statement==ID_label)
64 return to_code(operands().back()).last_statement();
65 }
66
67 return *this;
68}
69
73{
74 const irep_idt &statement=get_statement();
75
76 if(has_operands())
77 {
78 if(statement==ID_block)
79 return to_code(operands().back()).last_statement();
80 else if(statement==ID_label)
81 return to_code(operands().back()).last_statement();
82 }
83
84 return *this;
85}
86
89void code_blockt::append(const code_blockt &extra_block)
90{
91 statements().reserve(statements().size() + extra_block.statements().size());
92
93 for(const auto &statement : extra_block.statements())
94 {
95 add(statement);
96 }
97}
98
100{
101 codet *last=this;
102
103 while(true)
104 {
105 const irep_idt &statement=last->get_statement();
106
107 if(statement==ID_block &&
108 !to_code_block(*last).statements().empty())
109 {
110 last=&to_code_block(*last).statements().back();
111 }
112 else if(statement==ID_label)
113 {
114 last = &(to_code_label(*last).code());
115 }
116 else
117 break;
118 }
119
120 return *last;
121}
122
124 const exprt &condition, const source_locationt &loc)
125{
126 code_blockt result({code_assertt(condition), code_assumet(condition)});
127
128 for(auto &op : result.statements())
129 op.add_source_location() = loc;
130
131 result.add_source_location() = loc;
132
133 return result;
134}
135
137{
138 const auto &sub = find(ID_parameters).get_sub();
139 std::vector<irep_idt> result;
140 result.reserve(sub.size());
141 for(const auto &s : sub)
142 result.push_back(s.get(ID_identifier));
143 return result;
144}
145
147 const std::vector<irep_idt> &parameter_identifiers)
148{
149 auto &sub = add(ID_parameters).get_sub();
150 sub.reserve(parameter_identifiers.size());
151 for(const auto &id : parameter_identifiers)
152 {
153 sub.push_back(irept(ID_parameter));
154 sub.back().set(ID_identifier, id);
155 }
156}
157
159 exprt start_index,
160 exprt end_index,
161 symbol_exprt loop_index,
162 codet body,
163 source_locationt location)
164{
165 PRECONDITION(start_index.type() == loop_index.type());
166 PRECONDITION(end_index.type() == loop_index.type());
168 loop_index,
169 plus_exprt(loop_index, from_integer(1, loop_index.type())),
170 location);
171
172 return code_fort{
173 code_frontend_assignt{loop_index, std::move(start_index)},
174 binary_relation_exprt{loop_index, ID_lt, std::move(end_index)},
175 std::move(inc),
176 std::move(body)};
177}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition std_code.h:270
An assumption, which must hold in subsequent code.
Definition std_code.h:217
A codet representing sequential composition of program statements.
Definition std_code.h:130
code_operandst & statements()
Definition std_code.h:138
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition std_code.cpp:89
void add(const codet &code)
Definition std_code.h:168
codet & find_last_statement()
Definition std_code.cpp:99
codet representation of a for statement.
Definition std_code.h:734
static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)
Produce a code_fort representing:
Definition std_code.cpp:158
const codet & body() const
Definition std_code.h:779
A codet representing an assignment in the program.
Definition std_code.h:24
std::vector< irep_idt > get_parameter_identifiers() const
Definition std_code.cpp:136
void set_parameter_identifiers(const std::vector< irep_idt > &)
Definition std_code.cpp:146
codet & code()
Definition std_code.h:977
Data structure for representing an arbitrary statement in a program.
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them.
Definition std_code.cpp:21
exprt & op0()
Definition expr.h:99
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them.
Definition std_code.cpp:55
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:89
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
source_locationt & add_source_location()
Definition expr.h:235
irept()=default
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
subt & get_sub()
Definition irep.h:456
irept & add(const irep_idt &name)
Definition irep.cpp:116
The plus expression Associativity is not specified.
Definition std_expr.h:914
A side_effect_exprt that performs an assignment.
Definition std_code.h:1565
Expression to hold a symbol (variable)
Definition std_expr.h:80
API to expression classes for Pointers.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &loc)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
Definition std_code.cpp:123
const code_labelt & to_code_label(const codet &code)
Definition std_code.h:1004
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const codet & to_code(const exprt &expr)