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 
16 #include "loop_utils.h"
17 
19  const local_may_aliast &local_may_alias,
21  modifiest &modifies)
22 {
23  const goto_programt::instructiont &instruction=*i_it;
24 
25  if(instruction.is_assign())
26  {
27  const exprt &lhs=to_code_assign(instruction.code).lhs();
28  get_modifies_lhs(local_may_alias, i_it, lhs, modifies);
29  }
30  else if(instruction.is_function_call())
31  {
32  const code_function_callt &code_function_call=
33  to_code_function_call(instruction.code);
34  const exprt &lhs=code_function_call.lhs();
35 
36  // return value assignment
37  if(lhs.is_not_nil())
38  get_modifies_lhs(local_may_alias, i_it, lhs, modifies);
39 
41  code_function_call.function(), modifies);
42  }
43 }
44 
46  const exprt &function,
47  modifiest &modifies)
48 {
49  if(function.id()==ID_symbol)
50  {
51  const irep_idt &identifier=to_symbol_expr(function).get_identifier();
52 
53  function_mapt::const_iterator fm_it=
54  function_map.find(identifier);
55 
56  if(fm_it!=function_map.end())
57  {
58  // already done
59  modifies.insert(fm_it->second.begin(), fm_it->second.end());
60  return;
61  }
62 
63  goto_functionst::function_mapt::const_iterator
64  f_it=goto_functions.function_map.find(identifier);
65 
66  if(f_it==goto_functions.function_map.end())
67  return;
68 
69  local_may_aliast local_may_alias(f_it->second);
70 
71  const goto_programt &goto_program=f_it->second.body;
72 
73  forall_goto_program_instructions(i_it, goto_program)
74  get_modifies(local_may_alias, i_it, modifies);
75  }
76  else if(function.id()==ID_if)
77  {
78  get_modifies_function(to_if_expr(function).true_case(), modifies);
79  get_modifies_function(to_if_expr(function).false_case(), modifies);
80  }
81 }
exprt & lhs()
Definition: std_code.h:312
codet representation of a function call statement.
Definition: std_code.h:1215
exprt & function()
Definition: std_code.h:1250
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
const goto_functionst & goto_functions
function_mapt function_map
std::set< exprt > modifiest
void get_modifies_function(const exprt &, modifiest &)
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
function_mapt function_map
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst::const_iterator const_targett
Definition: goto_program.h:551
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & get_identifier() const
Definition: std_expr.h:110
#define forall_goto_program_instructions(it, program)
void get_modifies_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies)
Definition: loop_utils.cpp:58
Helper functions for k-induction and loop invariants.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190