cprover
escape_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-insensitive, location-sensitive escape analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "escape_analysis.h"
13 
14 #include <util/cprover_prefix.h>
15 #include <util/simplify_expr.h>
16 
18 {
19  const irep_idt &identifier=symbol.get_identifier();
20  if(
21  identifier == CPROVER_PREFIX "memory_leak" ||
22  identifier == CPROVER_PREFIX "malloc_object" ||
23  identifier == CPROVER_PREFIX "dead_object" ||
24  identifier == CPROVER_PREFIX "deallocated")
25  {
26  return false;
27  }
28 
29  return true;
30 }
31 
33 {
34  if(lhs.id()==ID_address_of)
35  return get_function(to_address_of_expr(lhs).object());
36  else if(lhs.id()==ID_typecast)
37  return get_function(to_typecast_expr(lhs).op());
38  else if(lhs.id()==ID_symbol)
39  {
40  irep_idt identifier=to_symbol_expr(lhs).get_identifier();
41  return identifier;
42  }
43 
44  return irep_idt();
45 }
46 
48  const exprt &lhs,
49  const std::set<irep_idt> &cleanup_functions)
50 {
51  if(lhs.id()==ID_symbol)
52  {
53  const symbol_exprt &symbol_expr=to_symbol_expr(lhs);
54  if(is_tracked(symbol_expr))
55  {
56  irep_idt identifier=symbol_expr.get_identifier();
57 
58  if(cleanup_functions.empty())
59  cleanup_map.erase(identifier);
60  else
61  cleanup_map[identifier].cleanup_functions=cleanup_functions;
62  }
63  }
64 }
65 
67  const exprt &lhs,
68  const std::set<irep_idt> &alias_set)
69 {
70  if(lhs.id()==ID_symbol)
71  {
72  const symbol_exprt &symbol_expr=to_symbol_expr(lhs);
73  if(is_tracked(symbol_expr))
74  {
75  irep_idt identifier=symbol_expr.get_identifier();
76 
77  aliases.isolate(identifier);
78 
79  for(const auto &alias : alias_set)
80  {
81  aliases.make_union(identifier, alias);
82  }
83  }
84  }
85 }
86 
88  const exprt &rhs,
89  std::set<irep_idt> &cleanup_functions)
90 {
91  if(rhs.id()==ID_symbol)
92  {
93  const symbol_exprt &symbol_expr=to_symbol_expr(rhs);
94  if(is_tracked(symbol_expr))
95  {
96  irep_idt identifier=symbol_expr.get_identifier();
97 
98  const escape_domaint::cleanup_mapt::const_iterator m_it=
99  cleanup_map.find(identifier);
100 
101  if(m_it!=cleanup_map.end())
102  cleanup_functions.insert(m_it->second.cleanup_functions.begin(),
103  m_it->second.cleanup_functions.end());
104  }
105  }
106  else if(rhs.id()==ID_if)
107  {
108  get_rhs_cleanup(to_if_expr(rhs).true_case(), cleanup_functions);
109  get_rhs_cleanup(to_if_expr(rhs).false_case(), cleanup_functions);
110  }
111  else if(rhs.id()==ID_typecast)
112  {
113  get_rhs_cleanup(to_typecast_expr(rhs).op(), cleanup_functions);
114  }
115 }
116 
118  const exprt &rhs,
119  std::set<irep_idt> &alias_set)
120 {
121  if(rhs.id()==ID_symbol)
122  {
123  const symbol_exprt &symbol_expr=to_symbol_expr(rhs);
124  if(is_tracked(symbol_expr))
125  {
126  irep_idt identifier=symbol_expr.get_identifier();
127  alias_set.insert(identifier);
128 
129  for(const auto &alias : aliases)
130  if(aliases.same_set(alias, identifier))
131  alias_set.insert(alias);
132  }
133  }
134  else if(rhs.id()==ID_if)
135  {
136  get_rhs_aliases(to_if_expr(rhs).true_case(), alias_set);
137  get_rhs_aliases(to_if_expr(rhs).false_case(), alias_set);
138  }
139  else if(rhs.id()==ID_typecast)
140  {
141  get_rhs_aliases(to_typecast_expr(rhs).op(), alias_set);
142  }
143  else if(rhs.id()==ID_address_of)
144  {
145  get_rhs_aliases_address_of(to_address_of_expr(rhs).op(), alias_set);
146  }
147 }
148 
150  const exprt &rhs,
151  std::set<irep_idt> &alias_set)
152 {
153  if(rhs.id()==ID_symbol)
154  {
155  irep_idt identifier=to_symbol_expr(rhs).get_identifier();
156  alias_set.insert("&"+id2string(identifier));
157  }
158  else if(rhs.id()==ID_if)
159  {
160  get_rhs_aliases_address_of(to_if_expr(rhs).true_case(), alias_set);
161  get_rhs_aliases_address_of(to_if_expr(rhs).false_case(), alias_set);
162  }
163  else if(rhs.id()==ID_dereference)
164  {
165  }
166 }
167 
169  const irep_idt &,
170  locationt from,
171  const irep_idt &,
172  locationt,
173  ai_baset &,
174  const namespacet &)
175 {
176  if(has_values.is_false())
177  return;
178 
179  // upcast of ai
180  // escape_analysist &ea=
181  // static_cast<escape_analysist &>(ai);
182 
183  const goto_programt::instructiont &instruction=*from;
184 
185  switch(instruction.type)
186  {
187  case ASSIGN:
188  {
189  const code_assignt &code_assign=to_code_assign(instruction.code);
190 
191  std::set<irep_idt> cleanup_functions;
192  get_rhs_cleanup(code_assign.rhs(), cleanup_functions);
193  assign_lhs_cleanup(code_assign.lhs(), cleanup_functions);
194 
195  std::set<irep_idt> rhs_aliases;
196  get_rhs_aliases(code_assign.rhs(), rhs_aliases);
197  assign_lhs_aliases(code_assign.lhs(), rhs_aliases);
198  }
199  break;
200 
201  case DECL:
202  {
203  const code_declt &code_decl=to_code_decl(instruction.code);
204  aliases.isolate(code_decl.get_identifier());
205  assign_lhs_cleanup(code_decl.symbol(), std::set<irep_idt>());
206  }
207  break;
208 
209  case DEAD:
210  {
211  const code_deadt &code_dead=to_code_dead(instruction.code);
212  aliases.isolate(code_dead.get_identifier());
213  assign_lhs_cleanup(code_dead.symbol(), std::set<irep_idt>());
214  }
215  break;
216 
217  case FUNCTION_CALL:
218  {
219  const code_function_callt &code_function_call=
220  to_code_function_call(instruction.code);
221  const exprt &function=code_function_call.function();
222 
223  if(function.id()==ID_symbol)
224  {
225  const irep_idt &identifier=to_symbol_expr(function).get_identifier();
226  if(identifier == CPROVER_PREFIX "cleanup")
227  {
228  if(code_function_call.arguments().size()==2)
229  {
230  exprt lhs=code_function_call.arguments()[0];
231 
232  irep_idt cleanup_function=
233  get_function(code_function_call.arguments()[1]);
234 
235  if(!cleanup_function.empty())
236  {
237  // may alias other stuff
238  std::set<irep_idt> lhs_set;
239  get_rhs_aliases(lhs, lhs_set);
240 
241  for(const auto &l : lhs_set)
242  {
243  cleanup_map[l].cleanup_functions.insert(cleanup_function);
244  }
245  }
246  }
247  }
248  }
249  }
250  break;
251 
252  case END_FUNCTION:
253  // This is the edge to the call site.
254  break;
255 
256  case GOTO: // Ignoring the guard is a valid over-approximation
257  break;
258  case CATCH:
259  case THROW:
260  DATA_INVARIANT(false, "Exceptions must be removed before analysis");
261  break;
262  case RETURN:
263  DATA_INVARIANT(false, "Returns must be removed before analysis");
264  break;
265  case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
266  case ATOMIC_END: // Ignoring is a valid over-approximation
267  case LOCATION: // No action required
268  case START_THREAD: // Require a concurrent analysis at higher level
269  case END_THREAD: // Require a concurrent analysis at higher level
270  case ASSERT: // No action required
271  case ASSUME: // Ignoring is a valid over-approximation
272  case SKIP: // No action required
273  break;
274  case OTHER:
275 #if 0
276  DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
277 #endif
278  break;
279  case INCOMPLETE_GOTO:
280  case NO_INSTRUCTION_TYPE:
281  DATA_INVARIANT(false, "Only complete instructions can be analyzed");
282  break;
283  }
284 }
285 
287  std::ostream &out,
288  const ai_baset &,
289  const namespacet &) const
290 {
291  if(has_values.is_known())
292  {
293  out << has_values.to_string() << '\n';
294  return;
295  }
296 
297  for(const auto &cleanup : cleanup_map)
298  {
299  out << cleanup.first << ':';
300  for(const auto &id : cleanup.second.cleanup_functions)
301  out << ' ' << id;
302  out << '\n';
303  }
304 
306  a_it1!=aliases.end();
307  a_it1++)
308  {
309  bool first=true;
310 
312  a_it2!=aliases.end();
313  a_it2++)
314  {
315  if(aliases.is_root(a_it1) && a_it1!=a_it2 &&
316  aliases.same_set(a_it1, a_it2))
317  {
318  if(first)
319  {
320  out << "Aliases: " << *a_it1;
321  first=false;
322  }
323  out << ' ' << *a_it2;
324  }
325  }
326 
327  if(!first)
328  out << '\n';
329  }
330 }
331 
333  const escape_domaint &b,
334  locationt,
335  locationt)
336 {
337  bool changed=has_values.is_false();
339 
340  for(const auto &cleanup : b.cleanup_map)
341  {
342  const std::set<irep_idt> &b_cleanup=cleanup.second.cleanup_functions;
343  std::set<irep_idt> &a_cleanup=cleanup_map[cleanup.first].cleanup_functions;
344  auto old_size=a_cleanup.size();
345  a_cleanup.insert(b_cleanup.begin(), b_cleanup.end());
346  if(a_cleanup.size()!=old_size)
347  changed=true;
348  }
349 
350  // kill empty ones
351 
352  for(cleanup_mapt::iterator a_it=cleanup_map.begin();
353  a_it!=cleanup_map.end();
354  ) // no a_it++
355  {
356  if(a_it->second.cleanup_functions.empty())
357  a_it=cleanup_map.erase(a_it);
358  else
359  a_it++;
360  }
361 
362  // do union
364  it!=b.aliases.end(); it++)
365  {
366  irep_idt b_root=b.aliases.find(it);
367 
368  if(!aliases.same_set(*it, b_root))
369  {
370  aliases.make_union(*it, b_root);
371  changed=true;
372  }
373  }
374 
375  // isolate non-tracked ones
376  #if 0
378  it!=aliases.end(); it++)
379  {
380  if(cleanup_map.find(*it)==cleanup_map.end())
381  aliases.isolate(it);
382  }
383  #endif
384 
385  return changed;
386 }
387 
389  const exprt &lhs,
390  std::set<irep_idt> &cleanup_functions) const
391 {
392  if(lhs.id()==ID_symbol)
393  {
394  const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
395 
396  // pointer with cleanup function?
397  const escape_domaint::cleanup_mapt::const_iterator m_it=
398  cleanup_map.find(identifier);
399 
400  if(m_it!=cleanup_map.end())
401  {
402  // count the aliases
403 
404  std::size_t count=0;
405 
406  for(const auto &alias : aliases)
407  {
408  if(alias!=identifier && aliases.same_set(alias, identifier))
409  count+=1;
410  }
411 
412  // There is an alias? Then we are still ok.
413  if(count==0)
414  {
415  cleanup_functions.insert(
416  m_it->second.cleanup_functions.begin(),
417  m_it->second.cleanup_functions.end());
418  }
419  }
420  }
421 }
422 
424  goto_functionst::goto_functiont &goto_function,
425  goto_programt::targett location,
426  const exprt &lhs,
427  const std::set<irep_idt> &cleanup_functions,
428  bool is_object,
429  const namespacet &ns)
430 {
431  source_locationt source_location=location->source_location;
432 
433  for(const auto &cleanup : cleanup_functions)
434  {
435  symbol_exprt function=ns.lookup(cleanup).symbol_expr();
436  const code_typet &function_type=to_code_type(function.type());
437 
438  goto_function.body.insert_before_swap(location);
439  code_function_callt code(function);
440  code.function().add_source_location()=source_location;
441 
442  if(function_type.parameters().size()==1)
443  {
444  typet param_type=function_type.parameters().front().type();
445  exprt arg=lhs;
446  if(is_object)
447  arg=address_of_exprt(arg);
448 
449  arg = typecast_exprt::conditional_cast(arg, param_type);
450 
451  code.arguments().push_back(arg);
452  }
453 
454  *location = goto_programt::make_function_call(code, source_location);
455  }
456 }
457 
459  goto_modelt &goto_model)
460 {
461  const namespacet ns(goto_model.symbol_table);
462 
463  Forall_goto_functions(f_it, goto_model.goto_functions)
464  {
465  Forall_goto_program_instructions(i_it, f_it->second.body)
466  {
467  get_state(i_it);
468 
469  const goto_programt::instructiont &instruction=*i_it;
470 
471  if(instruction.type == ASSIGN)
472  {
473  const code_assignt &code_assign = to_code_assign(instruction.code);
474 
475  std::set<irep_idt> cleanup_functions;
476  operator[](i_it).check_lhs(code_assign.lhs(), cleanup_functions);
478  f_it->second, i_it, code_assign.lhs(), cleanup_functions, false, ns);
479  }
480  else if(instruction.type == DEAD)
481  {
482  const code_deadt &code_dead = to_code_dead(instruction.code);
483 
484  std::set<irep_idt> cleanup_functions1;
485 
486  const escape_domaint &d = operator[](i_it);
487 
488  const escape_domaint::cleanup_mapt::const_iterator m_it =
489  d.cleanup_map.find("&" + id2string(code_dead.get_identifier()));
490 
491  // does it have a cleanup function for the object?
492  if(m_it != d.cleanup_map.end())
493  {
494  cleanup_functions1.insert(
495  m_it->second.cleanup_functions.begin(),
496  m_it->second.cleanup_functions.end());
497  }
498 
499  std::set<irep_idt> cleanup_functions2;
500 
501  d.check_lhs(code_dead.symbol(), cleanup_functions2);
502 
504  f_it->second, i_it, code_dead.symbol(), cleanup_functions1, true, ns);
506  f_it->second,
507  i_it,
508  code_dead.symbol(),
509  cleanup_functions2,
510  false,
511  ns);
512 
513  for(const auto &c : cleanup_functions1)
514  {
515  (void)c;
516  i_it++;
517  }
518 
519  for(const auto &c : cleanup_functions2)
520  {
521  (void)c;
522  i_it++;
523  }
524  }
525  }
526  }
527 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
escape_domaint
Definition: escape_analysis.h:25
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
escape_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Definition: escape_analysis.cpp:286
union_find::isolate
void isolate(typename numbering< T >::const_iterator it)
Definition: union_find.h:254
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:450
ait< escape_domaint >::operator[]
const escape_domaint & operator[](locationt l) const
Find the analysis result for a given location.
Definition: ai.h:587
typet
The type of an expression, extends irept.
Definition: type.h:29
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
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
escape_domaint::check_lhs
void check_lhs(const exprt &, std::set< irep_idt > &) const
Definition: escape_analysis.cpp:388
union_find::begin
iterator begin()
Definition: union_find.h:274
union_find::end
iterator end()
Definition: union_find.h:278
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
escape_domaint::get_rhs_aliases
void get_rhs_aliases(const exprt &, std::set< irep_idt > &)
Definition: escape_analysis.cpp:117
escape_domaint::assign_lhs_cleanup
void assign_lhs_cleanup(const exprt &, const std::set< irep_idt > &)
Definition: escape_analysis.cpp:47
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
irep_idt
dstringt irep_idt
Definition: irep.h:32
escape_domaint::get_rhs_cleanup
void get_rhs_cleanup(const exprt &, std::set< irep_idt > &)
Definition: escape_analysis.cpp:87
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
code_declt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:418
union_find::find
const T & find(typename numbering< T >::const_iterator it) const
Definition: union_find.h:192
tvt::is_known
bool is_known() const
Definition: threeval.h:28
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1049
THROW
@ THROW
Definition: goto_program.h:50
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
coverage_criteriont::LOCATION
@ LOCATION
GOTO
@ GOTO
Definition: goto_program.h:34
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
escape_domaint::aliases
aliasest aliases
Definition: escape_analysis.h:85
escape_domaint::get_function
irep_idt get_function(const exprt &)
Definition: escape_analysis.cpp:32
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
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
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
ait< escape_domaint >::get_state
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
Definition: ai.h:515
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
escape_domaint::get_rhs_aliases_address_of
void get_rhs_aliases_address_of(const exprt &, std::set< irep_idt > &)
Definition: escape_analysis.cpp:149
union_find::same_set
bool same_set(const T &a, const T &b) const
Definition: union_find.h:173
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
OTHER
@ OTHER
Definition: goto_program.h:37
escape_domaint::merge
bool merge(const escape_domaint &b, locationt from, locationt to)
Definition: escape_analysis.cpp:332
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:473
irept::id
const irep_idt & id() const
Definition: irep.h:418
escape_domaint::assign_lhs_aliases
void assign_lhs_aliases(const exprt &, const std::set< irep_idt > &)
Definition: escape_analysis.cpp:66
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
dstringt::empty
bool empty() const
Definition: dstring.h:88
tvt::to_string
const char * to_string() const
Definition: threeval.cpp:13
escape_analysist::instrument
void instrument(goto_modelt &)
Definition: escape_analysis.cpp:458
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
cprover_prefix.h
tvt::is_false
bool is_false() const
Definition: threeval.h:26
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
union_find::is_root
bool is_root(const T &a) const
Definition: union_find.h:222
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
source_locationt
Definition: source_location.h:20
simplify_expr.h
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
RETURN
@ RETURN
Definition: goto_program.h:45
union_find< irep_idt >::const_iterator
numbering_typet::const_iterator const_iterator
Definition: union_find.h:151
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
union_find::make_union
bool make_union(const T &a, const T &b)
Definition: union_find.h:154
escape_domaint::transform
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Definition: escape_analysis.cpp:168
escape_domaint::has_values
tvt has_values
Definition: escape_analysis.h:99
CATCH
@ CATCH
Definition: goto_program.h:51
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
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
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
START_THREAD
@ START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:44
DEAD
@ DEAD
Definition: goto_program.h:48
escape_analysist::insert_cleanup
void insert_cleanup(goto_functionst::goto_functiont &, goto_programt::targett, const exprt &, const std::set< irep_idt > &, bool is_object, const namespacet &)
Definition: escape_analysis.cpp:423
code_deadt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:483
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
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
ASSERT
@ ASSERT
Definition: goto_program.h:36
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
escape_domaint::cleanup_map
cleanup_mapt cleanup_map
Definition: escape_analysis.h:96
END_THREAD
@ END_THREAD
Definition: goto_program.h:40
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
escape_domaint::is_tracked
bool is_tracked(const symbol_exprt &)
Definition: escape_analysis.cpp:17
escape_analysis.h
Field-insensitive, location-sensitive, over-approximative escape analysis.