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 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
function_modifiest::function_map
function_mapt function_map
Definition: function_modifies.h:46
exprt
Base class for all expressions.
Definition: expr.h:53
function_modifiest::goto_functions
const goto_functionst & goto_functions
Definition: function_modifies.h:43
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
local_may_aliast
Definition: local_may_alias.h:26
function_modifies.h
Modifies.
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
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
get_modifies_lhs
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:57
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
loop_utils.h
Helper functions for k-induction and loop invariants.
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
function_modifiest::get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
Definition: function_modifies.cpp:18
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
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.
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
function_modifiest::modifiest
std::set< exprt > modifiest
Definition: function_modifies.h:26
function_modifiest::get_modifies_function
void get_modifies_function(const exprt &, modifiest &)
Definition: function_modifies.cpp:45