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 
18 #include "loop_utils.h"
19 
21  const local_may_aliast &local_may_alias,
23  modifiest &modifies)
24 {
25  const goto_programt::instructiont &instruction=*i_it;
26 
27  if(instruction.is_assign())
28  {
29  const exprt &lhs = instruction.get_assign().lhs();
30  get_modifies_lhs(local_may_alias, i_it, lhs, modifies);
31  }
32  else if(instruction.is_function_call())
33  {
34  const exprt &lhs = instruction.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 
40  get_modifies_function(instruction.call_function(), modifies);
41  }
42 }
43 
45  const exprt &function,
46  modifiest &modifies)
47 {
48  if(function.id()==ID_symbol)
49  {
50  const irep_idt &identifier=to_symbol_expr(function).get_identifier();
51 
52  function_mapt::const_iterator fm_it=
53  function_map.find(identifier);
54 
55  if(fm_it!=function_map.end())
56  {
57  // already done
58  modifies.insert(fm_it->second.begin(), fm_it->second.end());
59  return;
60  }
61 
62  goto_functionst::function_mapt::const_iterator
63  f_it=goto_functions.function_map.find(identifier);
64 
65  if(f_it==goto_functions.function_map.end())
66  return;
67 
68  local_may_aliast local_may_alias(f_it->second);
69 
70  const goto_programt &goto_program=f_it->second.body;
71 
72  forall_goto_program_instructions(i_it, goto_program)
73  get_modifies(local_may_alias, i_it, modifies);
74  }
75  else if(function.id()==ID_if)
76  {
77  get_modifies_function(to_if_expr(function).true_case(), modifies);
78  get_modifies_function(to_if_expr(function).false_case(), modifies);
79  }
80 }
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:2237
function_modifiest::function_map
function_mapt function_map
Definition: function_modifies.h:50
exprt
Base class for all expressions.
Definition: expr.h:54
function_modifiest::goto_functions
const goto_functionst & goto_functions
Definition: function_modifies.h:47
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1238
local_may_aliast
Definition: local_may_alias.h:26
goto_programt::instructiont::get_assign
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:198
function_modifies.h
Modifies.
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
local_may_alias.h
Field-insensitive, location-sensitive may-alias analysis.
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:40
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:310
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
goto_programt::instructiont::call_lhs
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:375
loop_utils.h
Helper functions for k-induction and loop invariants.
function_modifiest::get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const goto_programt::const_targett, modifiest &)
Definition: function_modifies.cpp:20
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:529
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:530
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
API to expression classes.
goto_programt::instructiont::call_function
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:361
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1255
function_modifiest::modifiest
std::set< exprt > modifiest
Definition: function_modifies.h:30
function_modifiest::get_modifies_function
void get_modifies_function(const exprt &, modifiest &)
Definition: function_modifies.cpp:44