cprover
local_may_alias.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive may-alias analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "local_may_alias.h"
13 
14 #include <iterator>
15 #include <algorithm>
16 
17 #include <util/arith_tools.h>
18 #include <util/std_expr.h>
19 #include <util/std_code.h>
20 
21 #include <util/c_types.h>
22 #include <langapi/language_util.h>
23 
26 {
27  bool changed=false;
28 
29  // do union; this should be amortized linear
30  for(std::size_t i=0; i<src.aliases.size(); i++)
31  {
32  std::size_t root=src.aliases.find(i);
33 
34  if(!aliases.same_set(i, root))
35  {
36  aliases.make_union(i, root);
37  changed=true;
38  }
39  }
40 
41  return changed;
42 }
43 
45  const exprt &lhs,
46  const exprt &rhs,
47  const loc_infot &loc_info_src,
48  loc_infot &loc_info_dest)
49 {
50  if(lhs.id()==ID_symbol)
51  {
52  if(lhs.type().id()==ID_pointer)
53  {
54  unsigned dest_pointer=objects.number(lhs);
55 
56  // isolate the lhs pointer
57  loc_info_dest.aliases.isolate(dest_pointer);
58 
59  object_sett rhs_set;
60  get_rec(rhs_set, rhs, loc_info_src);
61 
62  // make these all aliases
63  for(object_sett::const_iterator
64  p_it=rhs_set.begin();
65  p_it!=rhs_set.end();
66  p_it++)
67  {
68  loc_info_dest.aliases.make_union(dest_pointer, *p_it);
69  }
70  }
71  }
72  else if(lhs.id()==ID_dereference)
73  {
74  // this might invalidate all pointers that are
75  // a) local and dirty
76  // b) global
77  if(lhs.type().id()==ID_pointer)
78  {
79  for(std::size_t i=0; i<objects.size(); i++)
80  {
81  if(objects[i].id()==ID_symbol)
82  {
83  const irep_idt &identifier=
85 
86  if(dirty(identifier) || !locals.is_local(identifier))
87  {
88  loc_info_dest.aliases.isolate(i);
89  loc_info_dest.aliases.make_union(i, unknown_object);
90  }
91  }
92  }
93  }
94  }
95  else if(lhs.id()==ID_index)
96  {
97  assign_lhs(to_index_expr(lhs).array(), rhs, loc_info_src, loc_info_dest);
98  }
99  else if(lhs.id()==ID_member)
100  {
101  assign_lhs(
102  to_member_expr(lhs).struct_op(), rhs, loc_info_src, loc_info_dest);
103  }
104  else if(lhs.id()==ID_typecast)
105  {
106  assign_lhs(to_typecast_expr(lhs).op(), rhs, loc_info_src, loc_info_dest);
107  }
108  else if(lhs.id()==ID_if)
109  {
110  assign_lhs(to_if_expr(lhs).true_case(), rhs, loc_info_src, loc_info_dest);
111  assign_lhs(to_if_expr(lhs).false_case(), rhs, loc_info_src, loc_info_dest);
112  }
113 }
114 
115 std::set<exprt> local_may_aliast::get(
117  const exprt &rhs) const
118 {
119  local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
120 
121  assert(loc_it!=cfg.loc_map.end());
122 
123  const loc_infot &loc_info_src=loc_infos[loc_it->second];
124 
125  object_sett result_tmp;
126  get_rec(result_tmp, rhs, loc_info_src);
127 
128  std::set<exprt> result;
129 
130  for(object_sett::const_iterator
131  it=result_tmp.begin();
132  it!=result_tmp.end();
133  it++)
134  {
135  result.insert(objects[*it]);
136  }
137 
138  return result;
139 }
140 
143  const exprt &src1, const exprt &src2) const
144 {
145  local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t);
146 
147  assert(loc_it!=cfg.loc_map.end());
148 
149  const loc_infot &loc_info_src=loc_infos[loc_it->second];
150 
151  object_sett tmp1, tmp2;
152  get_rec(tmp1, src1, loc_info_src);
153  get_rec(tmp2, src2, loc_info_src);
154 
155  if(tmp1.find(unknown_object)!=tmp1.end() ||
156  tmp2.find(unknown_object)!=tmp2.end())
157  return true;
158 
159  std::list<unsigned> result;
160 
161  std::set_intersection(
162  tmp1.begin(), tmp1.end(),
163  tmp2.begin(), tmp2.end(),
164  std::back_inserter(result));
165 
166  return !result.empty();
167 }
168 
170  object_sett &dest,
171  const exprt &rhs,
172  const loc_infot &loc_info_src) const
173 {
174  if(rhs.id()==ID_constant)
175  {
176  if(rhs.is_zero())
177  dest.insert(objects.number(exprt(ID_null_object)));
178  else
179  dest.insert(objects.number(exprt(ID_integer_address_object)));
180  }
181  else if(rhs.id()==ID_symbol)
182  {
183  if(rhs.type().id()==ID_pointer)
184  {
185  unsigned src_pointer=objects.number(rhs);
186 
187  dest.insert(src_pointer);
188 
189  for(std::size_t i=0; i<loc_info_src.aliases.size(); i++)
190  if(loc_info_src.aliases.same_set(src_pointer, i))
191  dest.insert(i);
192  }
193  else
194  dest.insert(unknown_object);
195  }
196  else if(rhs.id()==ID_if)
197  {
198  get_rec(dest, to_if_expr(rhs).false_case(), loc_info_src);
199  get_rec(dest, to_if_expr(rhs).true_case(), loc_info_src);
200  }
201  else if(rhs.id()==ID_address_of)
202  {
203  const exprt &object=to_address_of_expr(rhs).object();
204 
205  if(object.id()==ID_symbol)
206  {
207  unsigned object_nr=objects.number(rhs);
208  dest.insert(object_nr);
209 
210  for(std::size_t i=0; i<loc_info_src.aliases.size(); i++)
211  if(loc_info_src.aliases.same_set(object_nr, i))
212  dest.insert(i);
213  }
214  else if(object.id()==ID_index)
215  {
216  const index_exprt &index_expr=to_index_expr(object);
217  if(index_expr.array().id()==ID_symbol)
218  {
219  index_exprt tmp1=index_expr;
220  tmp1.index()=from_integer(0, index_type());
221  address_of_exprt tmp2(tmp1);
222  unsigned object_nr=objects.number(tmp2);
223  dest.insert(object_nr);
224 
225  for(std::size_t i=0; i<loc_info_src.aliases.size(); i++)
226  if(loc_info_src.aliases.same_set(object_nr, i))
227  dest.insert(i);
228  }
229  else if(index_expr.array().id()==ID_string_constant)
230  {
231  index_exprt tmp1=index_expr;
232  tmp1.index()=from_integer(0, index_type());
233  address_of_exprt tmp2(tmp1);
234  unsigned object_nr=objects.number(tmp2);
235  dest.insert(object_nr);
236 
237  for(std::size_t i=0; i<loc_info_src.aliases.size(); i++)
238  if(loc_info_src.aliases.same_set(object_nr, i))
239  dest.insert(i);
240  }
241  else
242  dest.insert(unknown_object);
243  }
244  else
245  dest.insert(unknown_object);
246  }
247  else if(rhs.id()==ID_typecast)
248  {
249  get_rec(dest, to_typecast_expr(rhs).op(), loc_info_src);
250  }
251  else if(rhs.id()==ID_plus)
252  {
253  const auto &plus_expr = to_plus_expr(rhs);
254 
255  if(plus_expr.operands().size() >= 3)
256  {
258  plus_expr.op0().type().id() == ID_pointer,
259  "pointer in pointer-typed sum must be op0");
260  get_rec(dest, plus_expr.op0(), loc_info_src);
261  }
262  else if(plus_expr.operands().size() == 2)
263  {
264  // one must be pointer, one an integer
265  if(plus_expr.op0().type().id() == ID_pointer)
266  {
267  get_rec(dest, plus_expr.op0(), loc_info_src);
268  }
269  else if(plus_expr.op1().type().id() == ID_pointer)
270  {
271  get_rec(dest, plus_expr.op1(), loc_info_src);
272  }
273  else
274  dest.insert(unknown_object);
275  }
276  else
277  dest.insert(unknown_object);
278  }
279  else if(rhs.id()==ID_minus)
280  {
281  const auto &op0 = to_minus_expr(rhs).op0();
282 
283  if(op0.type().id() == ID_pointer)
284  {
285  get_rec(dest, op0, loc_info_src);
286  }
287  else
288  dest.insert(unknown_object);
289  }
290  else if(rhs.id()==ID_member)
291  {
292  dest.insert(unknown_object);
293  }
294  else if(rhs.id()==ID_index)
295  {
296  dest.insert(unknown_object);
297  }
298  else if(rhs.id()==ID_dereference)
299  {
300  dest.insert(unknown_object);
301  }
302  else if(rhs.id()==ID_side_effect)
303  {
304  const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs);
305  const irep_idt &statement=side_effect_expr.get_statement();
306 
307  if(statement==ID_allocate)
308  {
309  dest.insert(objects.number(exprt(ID_dynamic_object)));
310  }
311  else
312  dest.insert(unknown_object);
313  }
314  else if(rhs.is_nil())
315  {
316  // this means 'empty'
317  }
318  else
319  dest.insert(unknown_object);
320 }
321 
322 void local_may_aliast::build(const goto_functiont &goto_function)
323 {
324  if(cfg.nodes.empty())
325  return;
326 
327  work_queuet work_queue;
328 
329  // put all nodes into work queue
330  for(local_cfgt::node_nrt n=0; n<cfg.nodes.size(); n++)
331  work_queue.push(n);
332 
333  unknown_object=objects.number(exprt(ID_unknown));
334 
335  loc_infos.resize(cfg.nodes.size());
336 
337  (void)goto_function; // unused parameter
338 #if 0
339  // feed in sufficiently bad defaults
340  for(code_typet::parameterst::const_iterator
341  it=goto_function.type.parameters().begin();
342  it!=goto_function.type.parameters().end();
343  it++)
344  {
345  const irep_idt &identifier=it->get_identifier();
346  if(is_tracked(identifier))
347  loc_infos[0].points_to[objects.number(identifier)].objects.insert(
349  }
350 #endif
351 
352 #if 0
353  for(localst::locals_mapt::const_iterator
354  l_it=locals.locals_map.begin();
355  l_it!=locals.locals_map.end();
356  l_it++)
357  {
358  if(is_tracked(l_it->first))
359  loc_infos[0].aliases.make_union(
360  objects.number(l_it->second), unknown_object);
361  }
362 #endif
363 
364  while(!work_queue.empty())
365  {
366  local_cfgt::node_nrt loc_nr=work_queue.top();
367  const local_cfgt::nodet &node=cfg.nodes[loc_nr];
368  const goto_programt::instructiont &instruction=*node.t;
369  work_queue.pop();
370 
371  const loc_infot &loc_info_src=loc_infos[loc_nr];
372  loc_infot loc_info_dest=loc_infos[loc_nr];
373 
374  switch(instruction.type)
375  {
376  case ASSIGN:
377  {
378  const code_assignt &code_assign = to_code_assign(instruction.code);
379  assign_lhs(
380  code_assign.lhs(), code_assign.rhs(), loc_info_src, loc_info_dest);
381  break;
382  }
383 
384  case DECL:
385  {
386  const code_declt &code_decl = to_code_decl(instruction.code);
387  assign_lhs(code_decl.symbol(), nil_exprt(), loc_info_src, loc_info_dest);
388  break;
389  }
390 
391  case DEAD:
392  {
393  const code_deadt &code_dead = to_code_dead(instruction.code);
394  assign_lhs(code_dead.symbol(), nil_exprt(), loc_info_src, loc_info_dest);
395  break;
396  }
397 
398  case FUNCTION_CALL:
399  {
400  const code_function_callt &code_function_call =
401  to_code_function_call(instruction.code);
402  if(code_function_call.lhs().is_not_nil())
403  assign_lhs(
404  code_function_call.lhs(), nil_exprt(), loc_info_src, loc_info_dest);
405 
406  // this might invalidate all pointers that are
407  // a) local and dirty
408  // b) global
409  for(std::size_t i = 0; i < objects.size(); i++)
410  {
411  if(objects[i].id() == ID_symbol)
412  {
413  const irep_idt &identifier =
415 
416  if(dirty(identifier) || !locals.is_local(identifier))
417  {
418  loc_info_dest.aliases.isolate(i);
419  loc_info_dest.aliases.make_union(i, unknown_object);
420  }
421  }
422  }
423  break;
424  }
425 
426  case CATCH:
427  case THROW:
428  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
429  break;
430  case RETURN:
431 #if 0
432  DATA_INVARIANT(false, "Returns must be removed before analysis");
433 #endif
434  break;
435  case GOTO: // Ignoring the guard is a valid over-approximation
436  case START_THREAD: // Require a concurrent analysis at higher level
437  case END_THREAD: // Require a concurrent analysis at higher level
438  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
439  case ATOMIC_END: // Ignoring is a valid over-approximation
440  case LOCATION: // No action required
441  case SKIP: // No action required
442  case END_FUNCTION: // No action required
443  case ASSERT: // No action required
444  case ASSUME: // Ignoring is a valid over-approximation
445  break;
446  case OTHER:
447 #if 0
449  false, "Unclear what is a safe over-approximation of OTHER");
450 #endif
451  break;
452  case INCOMPLETE_GOTO:
453  case NO_INSTRUCTION_TYPE:
454  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
455  break;
456  }
457 
458  for(local_cfgt::successorst::const_iterator
459  it=node.successors.begin();
460  it!=node.successors.end();
461  it++)
462  {
463  if(loc_infos[*it].merge(loc_info_dest))
464  work_queue.push(*it);
465  }
466  }
467 }
468 
470  std::ostream &out,
471  const goto_functiont &goto_function,
472  const namespacet &ns) const
473 {
474  unsigned l=0;
475 
476  forall_goto_program_instructions(i_it, goto_function.body)
477  {
478  out << "**** " << i_it->source_location << "\n";
479 
480  const loc_infot &loc_info=loc_infos[l];
481 
482  for(std::size_t i=0; i<loc_info.aliases.size(); i++)
483  {
484  if(loc_info.aliases.count(i)!=1 &&
485  loc_info.aliases.find(i)==i) // root?
486  {
487  out << '{';
488  for(std::size_t j=0; j<loc_info.aliases.size(); j++)
489  if(loc_info.aliases.find(j)==i)
490  {
491  assert(j<objects.size());
492  irep_idt identifier;
493  if(objects[j].id() == ID_symbol)
494  identifier = to_symbol_expr(objects[j]).get_identifier();
495  out << ' ' << from_expr(ns, identifier, objects[j]);
496  }
497 
498  out << " }";
499  out << "\n";
500  }
501  }
502 
503  out << "\n";
504  goto_function.body.output_instruction(ns, irep_idt(), out, *i_it);
505  out << "\n";
506 
507  l++;
508  }
509 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
local_may_aliast::output
void output(std::ostream &out, const goto_functiont &goto_function, const namespacet &ns) const
Definition: local_may_alias.cpp:469
local_may_aliast::loc_infos
loc_infost loc_infos
Definition: local_may_alias.h:77
unsigned_union_find::find
size_type find(size_type a) const
Definition: union_find.cpp:141
local_may_aliast::unknown_object
unsigned unknown_object
Definition: local_may_alias.h:92
arith_tools.h
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:450
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
local_cfgt::loc_map
loc_mapt loc_map
Definition: local_cfg.h:33
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:272
unsigned_union_find::size
size_type size() const
Definition: union_find.h:98
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
local_may_aliast::dirty
dirtyt dirty
Definition: local_may_alias.h:44
exprt
Base class for all expressions.
Definition: expr.h:53
irep_idt
dstringt irep_idt
Definition: irep.h:32
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1931
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:965
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
merge
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Definition: string_constraint_generator_main.cpp:100
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
THROW
@ THROW
Definition: goto_program.h:50
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
coverage_criteriont::LOCATION
@ LOCATION
GOTO
@ GOTO
Definition: goto_program.h:34
unsigned_union_find::count
size_type count(size_type a) const
Definition: union_find.h:104
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
unsigned_union_find::make_union
void make_union(size_type a, size_type b)
Definition: union_find.cpp:13
local_may_aliast::locals
localst locals
Definition: local_may_alias.h:45
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:41
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
language_util.h
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:519
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:920
local_may_aliast::aliases
bool aliases(const goto_programt::const_targett t, const exprt &src1, const exprt &src2) const
Definition: local_may_alias.cpp:141
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
local_may_aliast::build
void build(const goto_functiont &goto_function)
Definition: local_may_alias.cpp:322
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
local_cfgt::nodes
nodest nodes
Definition: local_cfg.h:36
localst::is_local
bool is_local(const irep_idt &identifier) const
Definition: locals.h:32
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
OTHER
@ OTHER
Definition: goto_program.h:37
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:473
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
local_cfgt::nodet
Definition: local_cfg.h:26
local_may_aliast::work_queuet
std::stack< local_cfgt::node_nrt > work_queuet
Definition: local_may_alias.h:61
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:42
SKIP
@ SKIP
Definition: goto_program.h:38
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:467
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
local_may_aliast::assign_lhs
void assign_lhs(const exprt &lhs, const exprt &rhs, const loc_infot &loc_info_src, loc_infot &loc_info_dest)
Definition: local_may_alias.cpp:44
std_code.h
unsigned_union_find::same_set
bool same_set(size_type a, size_type b) const
Definition: union_find.h:92
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
local_may_aliast::loc_infot::merge
bool merge(const loc_infot &src)
Definition: local_may_alias.cpp:25
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1897
local_may_aliast::loc_infot::aliases
alias_sett aliases
Definition: local_may_alias.h:71
RETURN
@ RETURN
Definition: goto_program.h:45
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
local_cfgt::node_nrt
std::size_t node_nrt
Definition: local_cfg.h:22
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
CATCH
@ CATCH
Definition: goto_program.h:51
local_may_aliast::objects
numbering< exprt > objects
Definition: local_may_alias.h:63
DECL
@ DECL
Definition: goto_program.h:47
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
ASSUME
@ ASSUME
Definition: goto_program.h:35
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
local_may_aliast::object_sett
std::set< unsigned > object_sett
Definition: local_may_alias.h:85
local_cfgt::nodet::successors
successorst successors
Definition: local_cfg.h:29
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
local_may_aliast::cfg
local_cfgt cfg
Definition: local_may_alias.h:46
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
DEAD
@ DEAD
Definition: goto_program.h:48
goto_functiont::type
code_typet type
The type of the function, indicating the return type and parameter types.
Definition: goto_function.h:34
local_cfgt::nodet::t
goto_programt::const_targett t
Definition: local_cfg.h:28
index_exprt
Array index operator.
Definition: std_expr.h:1293
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:43
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
local_may_aliast::get
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
Definition: local_may_alias.cpp:115
ASSERT
@ ASSERT
Definition: goto_program.h:36
unsigned_union_find::isolate
void isolate(size_type a)
Definition: union_find.cpp:41
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
std_expr.h
API to expression classes.
c_types.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
local_may_aliast::loc_infot
Definition: local_may_alias.h:69
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
local_may_aliast::get_rec
void get_rec(object_sett &dest, const exprt &rhs, const loc_infot &loc_info_src) const
Definition: local_may_alias.cpp:169