cprover
std_code.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #include "std_code.h"
11 
12 #include "std_expr.h"
13 
15 {
17 }
18 
20 {
22 }
23 
25 {
26  if(get_statement()==ID_block)
27  return static_cast<code_blockt &>(*this);
28 
29  exprt tmp;
30  tmp.swap(*this);
31 
32  *this = codet(ID_block);
33  move_to_operands(tmp);
34 
35  return static_cast<code_blockt &>(*this);
36 }
37 
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 
54 {
55  const irep_idt &statement=get_statement();
56 
57  if(has_operands())
58  {
59  if(statement==ID_block)
60  return to_code(op0()).first_statement();
61  else if(statement==ID_label)
62  return to_code(op0()).first_statement();
63  }
64 
65  return *this;
66 }
67 
69 {
70  const irep_idt &statement=get_statement();
71 
72  if(has_operands())
73  {
74  if(statement==ID_block)
75  return to_code(operands().back()).last_statement();
76  else if(statement==ID_label)
77  return to_code(operands().back()).last_statement();
78  }
79 
80  return *this;
81 }
82 
84 {
85  const irep_idt &statement=get_statement();
86 
87  if(has_operands())
88  {
89  if(statement==ID_block)
90  return to_code(operands().back()).last_statement();
91  else if(statement==ID_label)
92  return to_code(operands().back()).last_statement();
93  }
94 
95  return *this;
96 }
97 
100 void code_blockt::append(const code_blockt &extra_block)
101 {
102  operands().reserve(operands().size()+extra_block.operands().size());
103 
104  for(const auto &operand : extra_block.operands())
105  {
106  add(to_code(operand));
107  }
108 }
109 
111  const exprt &condition, const source_locationt &loc)
112 {
113  code_blockt result;
114  result.copy_to_operands(code_assertt(condition));
115  result.copy_to_operands(code_assumet(condition));
116  for(auto &op : result.operands())
117  op.add_source_location() = loc;
118  result.add_source_location() = loc;
119  return result;
120 }
121 
123  const irep_idt &statement,
124  const typet &_type,
125  const source_locationt &loc)
126  : exprt(ID_side_effect, _type)
127 {
128  set_statement(statement);
130 }
131 
133  const typet &_type,
134  const source_locationt &loc)
135  : side_effect_exprt(ID_nondet, _type, loc)
136 {
137  set_nullable(true);
138 }
139 
141  const exprt &_function,
142  const exprt::operandst &_arguments,
143  const typet &_type,
144  const source_locationt &loc)
145  : side_effect_exprt(ID_function_call, _type, loc)
146 {
147  operands().resize(2);
148  op1().id(ID_arguments);
149  function() = _function;
150  arguments() = _arguments;
151 }
#define loc()
const irep_idt & get_statement() const
Definition: std_code.h:40
The type of an expression.
Definition: type.h:22
const irep_idt & get_identifier() const
Definition: std_code.cpp:19
exprt & op0()
Definition: expr.h:72
exprt & symbol()
Definition: std_code.h:268
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
const irep_idt & get_identifier() const
Definition: std_expr.h:128
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
codet & first_statement()
Definition: std_code.cpp:38
side_effect_exprt(const irep_idt &statement)
Definition: std_code.h:1275
void set_nullable(bool nullable)
Definition: std_code.h:1358
const irep_idt & id() const
Definition: irep.h:259
void add(const codet &code)
Definition: std_code.h:112
class code_blockt & make_block()
Definition: std_code.cpp:24
codet & last_statement()
Definition: std_code.cpp:68
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:110
API to expression classes.
const irep_idt & get_identifier() const
Definition: std_code.cpp:14
exprt & op1()
Definition: expr.h:75
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:100
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
exprt & symbol()
Definition: std_code.h:321
bool has_operands() const
Definition: expr.h:63
std::vector< exprt > operandst
Definition: expr.h:45
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:404
An assumption, which must hold in subsequent code.
Definition: std_code.h:357
Base class for all expressions.
Definition: expr.h:42
codet()
Definition: std_code.h:25
exprt::operandst & arguments()
Definition: std_code.h:1453
void swap(irept &irep)
Definition: irep.h:303
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:89
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
A statement in a programming language.
Definition: std_code.h:21
An expression containing a side effect.
Definition: std_code.h:1271
operandst & operands()
Definition: expr.h:66
void set_statement(const irep_idt &statement)
Definition: std_code.h:1297