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 }
const irep_idt & get_statement() const
Definition: std_code.h:56
exprt & op0()
Definition: expr.h:84
codet & find_last_statement()
Definition: std_code.cpp:112
code_operandst & statements()
Definition: std_code.h:159
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
void add(const codet &code)
Definition: std_code.h:189
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:1289
API to expression classes.
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
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:548
An assumption, which must hold in subsequent code.
Definition: std_code.h:496
Base class for all expressions.
Definition: expr.h:54
codet()
Definition: std_code.h:38
void swap(irept &irep)
Definition: irep.h:300
source_locationt & add_source_location()
Definition: expr.h:233
A codet representing sequential composition of program statements.
Definition: std_code.h:150
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
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:1310
operandst & operands()
Definition: expr.h:78