CBMC
function_assigns.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Compute objects assigned to in a function
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "function_assigns.h"
13 
14 #include <util/std_expr.h>
15 
17 
18 #include "loop_utils.h"
19 
21  const local_may_aliast &local_may_alias,
23  assignst &assigns)
24 {
25  const goto_programt::instructiont &instruction = *i_it;
26 
27  if(instruction.is_assign())
28  {
29  get_assigns_lhs(local_may_alias, i_it, instruction.assign_lhs(), assigns);
30  }
31  else if(instruction.is_function_call())
32  {
33  const exprt &lhs = instruction.call_lhs();
34 
35  // return value assignment
36  if(lhs.is_not_nil())
37  get_assigns_lhs(local_may_alias, i_it, lhs, assigns);
38 
39  get_assigns_function(instruction.call_function(), assigns);
40  }
41 }
42 
44  const exprt &function,
45  assignst &assigns)
46 {
47  if(function.id() == ID_symbol)
48  {
49  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
50 
51  function_mapt::const_iterator fm_it = function_map.find(identifier);
52 
53  if(fm_it != function_map.end())
54  {
55  // already done
56  assigns.insert(fm_it->second.begin(), fm_it->second.end());
57  return;
58  }
59 
60  goto_functionst::function_mapt::const_iterator f_it =
61  goto_functions.function_map.find(identifier);
62 
63  if(f_it == goto_functions.function_map.end())
64  return;
65 
66  local_may_aliast local_may_alias(f_it->second);
67 
68  const goto_programt &goto_program = f_it->second.body;
69 
70  forall_goto_program_instructions(i_it, goto_program)
71  get_assigns(local_may_alias, i_it, assigns);
72  }
73  else if(function.id() == ID_if)
74  {
75  get_assigns_function(to_if_expr(function).true_case(), assigns);
76  get_assigns_function(to_if_expr(function).false_case(), assigns);
77  }
78 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
void get_assigns(const local_may_aliast &local_may_alias, const goto_programt::const_targett, assignst &)
function_mapt function_map
const goto_functionst & goto_functions
std::set< exprt > assignst
void get_assigns_function(const exprt &, assignst &)
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:286
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:272
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:200
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::const_iterator const_targett
Definition: goto_program.h:615
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & get_identifier() const
Definition: std_expr.h:160
Compute objects assigned to in a function.
#define forall_goto_program_instructions(it, program)
Field-insensitive, location-sensitive may-alias analysis.
void get_assigns_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns)
Definition: loop_utils.cpp:39
Helper functions for k-induction and loop invariants.
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272