CBMC
std_code.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Data structures representing statements in a program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "std_code.h"
13 
14 #include "arith_tools.h"
15 
19 {
20  const irep_idt &statement=get_statement();
21 
22  if(has_operands())
23  {
24  if(statement==ID_block)
25  return to_code(op0()).first_statement();
26  else if(statement==ID_label)
27  return to_code(op0()).first_statement();
28  }
29 
30  return *this;
31 }
32 
36 {
37  const irep_idt &statement=get_statement();
38 
39  if(has_operands())
40  {
41  if(statement==ID_block)
42  return to_code(op0()).first_statement();
43  else if(statement==ID_label)
44  return to_code(op0()).first_statement();
45  }
46 
47  return *this;
48 }
49 
53 {
54  const irep_idt &statement=get_statement();
55 
56  if(has_operands())
57  {
58  if(statement==ID_block)
59  return to_code(operands().back()).last_statement();
60  else if(statement==ID_label)
61  return to_code(operands().back()).last_statement();
62  }
63 
64  return *this;
65 }
66 
70 {
71  const irep_idt &statement=get_statement();
72 
73  if(has_operands())
74  {
75  if(statement==ID_block)
76  return to_code(operands().back()).last_statement();
77  else if(statement==ID_label)
78  return to_code(operands().back()).last_statement();
79  }
80 
81  return *this;
82 }
83 
86 void code_blockt::append(const code_blockt &extra_block)
87 {
88  statements().reserve(statements().size() + extra_block.statements().size());
89 
90  for(const auto &statement : extra_block.statements())
91  {
92  add(statement);
93  }
94 }
95 
97 {
98  codet *last=this;
99 
100  while(true)
101  {
102  const irep_idt &statement=last->get_statement();
103 
104  if(statement==ID_block &&
105  !to_code_block(*last).statements().empty())
106  {
107  last=&to_code_block(*last).statements().back();
108  }
109  else if(statement==ID_label)
110  {
111  last = &(to_code_label(*last).code());
112  }
113  else
114  break;
115  }
116 
117  return *last;
118 }
119 
121  const exprt &condition, const source_locationt &loc)
122 {
123  code_blockt result({code_assertt(condition), code_assumet(condition)});
124 
125  for(auto &op : result.statements())
126  op.add_source_location() = loc;
127 
128  result.add_source_location() = loc;
129 
130  return result;
131 }
132 
134 {
135  const auto &sub = find(ID_parameters).get_sub();
136  std::vector<irep_idt> result;
137  result.reserve(sub.size());
138  for(const auto &s : sub)
139  result.push_back(s.get(ID_identifier));
140  return result;
141 }
142 
144  const std::vector<irep_idt> &parameter_identifiers)
145 {
146  auto &sub = add(ID_parameters).get_sub();
147  sub.reserve(parameter_identifiers.size());
148  for(const auto &id : parameter_identifiers)
149  {
150  sub.push_back(irept(ID_parameter));
151  sub.back().set(ID_identifier, id);
152  }
153 }
154 
156  exprt start_index,
157  exprt end_index,
158  symbol_exprt loop_index,
159  codet body,
160  source_locationt location)
161 {
162  PRECONDITION(start_index.type() == loop_index.type());
163  PRECONDITION(end_index.type() == loop_index.type());
165  loop_index,
166  plus_exprt(loop_index, from_integer(1, loop_index.type())),
167  location);
168 
169  return code_fort{
170  code_frontend_assignt{loop_index, std::move(start_index)},
171  binary_relation_exprt{loop_index, ID_lt, std::move(end_index)},
172  std::move(inc),
173  std::move(body)};
174 }
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:762
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
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:86
void add(const codet &code)
Definition: std_code.h:168
code_operandst & statements()
Definition: std_code.h:138
codet & find_last_statement()
Definition: std_code.cpp:96
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:155
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:133
void set_parameter_identifiers(const std::vector< irep_idt > &)
Definition: std_code.cpp:143
codet & code()
Definition: std_code.h:977
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them.
Definition: std_code.cpp:18
exprt & op0()
Definition: expr.h:133
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them.
Definition: std_code.cpp:52
const irep_idt & get_statement() const
Definition: std_code_base.h:65
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
source_locationt & add_source_location()
Definition: expr.h:236
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
irept()=default
subt & get_sub()
Definition: irep.h:448
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
irept & add(const irep_idt &name)
Definition: irep.cpp:103
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
A side_effect_exprt that performs an assignment.
Definition: std_code.h:1565
Expression to hold a symbol (variable)
Definition: std_expr.h:131
#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:120
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)