cprover
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 "std_expr.h"
15 
21 {
22  if(get_statement()==ID_block)
23  return static_cast<code_blockt &>(*this);
24 
25  exprt tmp;
26  tmp.swap(*this);
27 
28  *this = codet(ID_block);
29  move_to_operands(tmp);
30 
31  return static_cast<code_blockt &>(*this);
32 }
33 
37 {
38  const irep_idt &statement=get_statement();
39 
40  if(has_operands())
41  {
42  if(statement==ID_block)
43  return to_code(op0()).first_statement();
44  else if(statement==ID_label)
45  return to_code(op0()).first_statement();
46  }
47 
48  return *this;
49 }
50 
53 {
54  const irep_idt &statement=get_statement();
55 
56  if(has_operands())
57  {
58  if(statement==ID_block)
59  return to_code(op0()).first_statement();
60  else if(statement==ID_label)
61  return to_code(op0()).first_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 {
87  const irep_idt &statement=get_statement();
88 
89  if(has_operands())
90  {
91  if(statement==ID_block)
92  return to_code(operands().back()).last_statement();
93  else if(statement==ID_label)
94  return to_code(operands().back()).last_statement();
95  }
96 
97  return *this;
98 }
99 
102 void code_blockt::append(const code_blockt &extra_block)
103 {
104  statements().reserve(statements().size() + extra_block.statements().size());
105 
106  for(const auto &statement : extra_block.statements())
107  {
108  add(statement);
109  }
110 }
111 
113 {
114  codet *last=this;
115 
116  while(true)
117  {
118  const irep_idt &statement=last->get_statement();
119 
120  if(statement==ID_block &&
121  !to_code_block(*last).statements().empty())
122  {
123  last=&to_code_block(*last).statements().back();
124  }
125  else if(statement==ID_label)
126  {
127  last = &(to_code_label(*last).code());
128  }
129  else
130  break;
131  }
132 
133  return *last;
134 }
135 
137  const exprt &condition, const source_locationt &loc)
138 {
139  code_blockt result({code_assertt(condition), code_assumet(condition)});
140 
141  for(auto &op : result.statements())
142  op.add_source_location() = loc;
143 
144  result.add_source_location() = loc;
145 
146  return result;
147 }
148 
150  const irep_idt &statement,
151  const typet &_type,
152  const source_locationt &loc)
153  : exprt(ID_side_effect, _type)
154 {
155  set_statement(statement);
156  add_source_location() = loc;
157 }
158 
160  const typet &_type,
161  const source_locationt &loc)
162  : side_effect_exprt(ID_nondet, _type, loc)
163 {
164  set_nullable(true);
165 }
166 
168  const exprt &_function,
169  const exprt::operandst &_arguments,
170  const typet &_type,
171  const source_locationt &loc)
172  : side_effect_exprt(ID_function_call, _type, loc)
173 {
174  operands().resize(2);
175  op1().id(ID_arguments);
176  function() = _function;
177  arguments() = _arguments;
178 }
const irep_idt & get_statement() const
Definition: std_code.h:56
The type of an expression, extends irept.
Definition: type.h:27
exprt & op0()
Definition: expr.h:84
codet & find_last_statement()
Definition: std_code.cpp:112
code_operandst & statements()
Definition: std_code.h:161
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt&#39;s operands.
Definition: expr.cpp:29
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them...
Definition: std_code.cpp:36
side_effect_exprt(const irep_idt &statement)
Definition: std_code.h:1432
void set_nullable(bool nullable)
Definition: std_code.h:1514
const irep_idt & id() const
Definition: irep.h:259
void add(const codet &code)
Definition: std_code.h:191
class code_blockt & make_block()
If this codet is a code_blockt (i.e. it represents a block of statements), return the unmodified inpu...
Definition: std_code.cpp:20
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them...
Definition: std_code.cpp:69
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:136
codet & code()
Definition: std_code.h:1157
API to expression classes.
exprt & op1()
Definition: expr.h:87
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:102
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
std::vector< exprt > operandst
Definition: expr.h:57
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:516
An assumption, which must hold in subsequent code.
Definition: std_code.h:469
Base class for all expressions.
Definition: expr.h:54
codet()
Definition: std_code.h:38
exprt::operandst & arguments()
Definition: std_code.h:1608
void swap(irept &irep)
Definition: irep.h:303
source_locationt & add_source_location()
Definition: expr.h:236
A codet representing sequential composition of program statements.
Definition: std_code.h:152
const codet & to_code(const exprt &expr)
Definition: std_code.h:138
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:226
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1178
An expression containing a side effect.
Definition: std_code.h:1428
operandst & operands()
Definition: expr.h:78
void set_statement(const irep_idt &statement)
Definition: std_code.h:1454