cprover
parameter_assignments.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Add parameter assignments
4 
5 Author: Daniel Kroening
6 
7 Date: September 2015
8 
9 \*******************************************************************/
10 
13 
14 #include "parameter_assignments.h"
15 
16 #include <util/std_expr.h>
17 #include <util/symbol_table.h>
18 
20 {
21 public:
22  explicit parameter_assignmentst(symbol_tablet &_symbol_table):
23  symbol_table(_symbol_table)
24  {
25  }
26 
27  void operator()(
28  goto_functionst &goto_functions);
29 
30 protected:
32 
33  void do_function_calls(
34  goto_functionst &goto_functions,
36 };
37 
40  goto_functionst &goto_functions,
42 {
44  {
45  if(i_it->is_function_call())
46  {
47  code_function_callt &function_call=to_code_function_call(i_it->code);
48 
49  // add x=y for f(y) where x is the parameter
50 
51  assert(function_call.function().id()==ID_symbol);
52 
53  const irep_idt &identifier=
54  to_symbol_expr(function_call.function()).get_identifier();
55 
56  // see if we have it
57  const namespacet ns(symbol_table);
58  const symbolt &function_symbol=ns.lookup(identifier);
59  const code_typet &code_type=to_code_type(function_symbol.type);
60 
61  goto_programt tmp;
62 
63  for(std::size_t nr=0; nr<code_type.parameters().size(); nr++)
64  {
65  irep_idt p_identifier=code_type.parameters()[nr].get_identifier();
66 
67  if(p_identifier.empty())
68  continue;
69 
70  if(nr<function_call.arguments().size())
71  {
73  t->make_assignment();
74  t->source_location=i_it->source_location;
75  const symbolt &lhs_symbol=ns.lookup(p_identifier);
76  symbol_exprt lhs=lhs_symbol.symbol_expr();
77  exprt rhs=function_call.arguments()[nr];
78  if(rhs.type()!=lhs.type())
79  rhs.make_typecast(lhs.type());
80  t->code=code_assignt(lhs, rhs);
81  t->function=i_it->function;
82  }
83  }
84 
85  std::size_t count=tmp.instructions.size();
87 
88  for(; count!=0; count--) i_it++;
89  }
90  }
91 }
92 
94 {
95  Forall_goto_functions(it, goto_functions)
96  do_function_calls(goto_functions, it->second.body);
97 }
98 
101  symbol_tablet &symbol_table,
102  goto_functionst &goto_functions)
103 {
104  parameter_assignmentst rr(symbol_table);
105  rr(goto_functions);
106 }
107 
110 {
111  parameter_assignmentst rr(goto_model.symbol_table);
112  rr(goto_model.goto_functions);
113 }
Base type of functions.
Definition: std_types.h:764
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
void operator()(goto_functionst &goto_functions)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
typet & type()
Definition: expr.h:56
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void do_function_calls(goto_functionst &goto_functions, goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
const irep_idt & id() const
Definition: irep.h:189
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
argumentst & arguments()
Definition: std_code.h:860
instructionst::iterator targett
Definition: goto_program.h:397
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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
Author: Diffblue Ltd.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
exprt & function()
Definition: std_code.h:848
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
#define Forall_goto_functions(it, functions)
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
parameter_assignmentst(symbol_tablet &_symbol_table)
Add parameter assignments.
bool empty() const
Definition: dstring.h:61
void make_typecast(const typet &_type)
Definition: expr.cpp:84
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879