cprover
function_modifies.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Modifies
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "function_modifies.h"
13 
14 #include <util/std_expr.h>
15 
17  const local_may_aliast &local_may_alias,
19  const exprt &lhs,
20  modifiest &modifies)
21 {
22  if(lhs.id()==ID_symbol)
23  modifies.insert(lhs);
24  else if(lhs.id()==ID_dereference)
25  {
26  modifiest m=local_may_alias.get(t, to_dereference_expr(lhs).pointer());
27  for(modifiest::const_iterator m_it=m.begin();
28  m_it!=m.end(); m_it++)
29  get_modifies_lhs(local_may_alias, t, *m_it, modifies);
30  }
31  else if(lhs.id()==ID_member)
32  {
33  }
34  else if(lhs.id()==ID_index)
35  {
36  }
37  else if(lhs.id()==ID_if)
38  {
39  get_modifies_lhs(local_may_alias, t, to_if_expr(lhs).true_case(), modifies);
41  local_may_alias, t, to_if_expr(lhs).false_case(), modifies);
42  }
43 }
44 
46  const local_may_aliast &local_may_alias,
48  modifiest &modifies)
49 {
50  const goto_programt::instructiont &instruction=*i_it;
51 
52  if(instruction.is_assign())
53  {
54  const exprt &lhs=to_code_assign(instruction.code).lhs();
55  get_modifies_lhs(local_may_alias, i_it, lhs, modifies);
56  }
57  else if(instruction.is_function_call())
58  {
59  const code_function_callt &code_function_call=
60  to_code_function_call(instruction.code);
61  const exprt &lhs=code_function_call.lhs();
62 
63  // return value assignment
64  if(lhs.is_not_nil())
65  get_modifies_lhs(local_may_alias, i_it, lhs, modifies);
66 
68  code_function_call.function(), modifies);
69  }
70 }
71 
73  const exprt &function,
74  modifiest &modifies)
75 {
76  if(function.id()==ID_symbol)
77  {
78  const irep_idt &identifier=to_symbol_expr(function).get_identifier();
79 
80  function_mapt::const_iterator fm_it=
81  function_map.find(identifier);
82 
83  if(fm_it!=function_map.end())
84  {
85  // already done
86  modifies.insert(fm_it->second.begin(), fm_it->second.end());
87  return;
88  }
89 
90  goto_functionst::function_mapt::const_iterator
91  f_it=goto_functions.function_map.find(identifier);
92 
93  if(f_it==goto_functions.function_map.end())
94  return;
95 
96  local_may_aliast local_may_alias(f_it->second);
97 
98  const goto_programt &goto_program=f_it->second.body;
99 
101  get_modifies(local_may_alias, i_it, modifies);
102  }
103  else if(function.id()==ID_if)
104  {
105  get_modifies_function(to_if_expr(function).true_case(), modifies);
106  get_modifies_function(to_if_expr(function).false_case(), modifies);
107  }
108 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
std::set< exprt > modifiest
bool is_not_nil() const
Definition: irep.h:103
const irep_idt & get_identifier() const
Definition: std_expr.h:128
function_mapt function_map
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
void get_modifies_lhs(const local_may_aliast &, const goto_programt::const_targett, const exprt &lhs, modifiest &)
API to expression classes.
instructionst::const_iterator const_targett
Definition: goto_program.h:398
A function call.
Definition: std_code.h:828
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
exprt & function()
Definition: std_code.h:848
Base class for all expressions.
Definition: expr.h:42
const goto_functionst & goto_functions
function_mapt function_map
goto_programt & goto_program
Definition: cover.cpp:63
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
void get_modifies_function(const exprt &, modifiest &)
std::set< exprt > get(const goto_programt::const_targett t, const exprt &src) const
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879