cprover
Loading...
Searching...
No Matches
parameter_assignments.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Add parameter assignments
4
5Author: Daniel Kroening
6
7Date: September 2015
8
9\*******************************************************************/
10
13
15
16#include <util/std_expr.h>
17#include <util/symbol_table.h>
18
19#include "goto_model.h"
20
22{
23public:
28
29 void operator()(
30 goto_functionst &goto_functions);
31
32protected:
34
36 goto_programt &goto_program);
37};
38
41 goto_programt &goto_program)
42{
44 {
45 if(i_it->is_function_call())
46 {
47 // add x=y for f(y) where x is the parameter
48 PRECONDITION(as_const(*i_it).call_function().id() == ID_symbol);
49
50 const irep_idt &identifier =
51 to_symbol_expr(as_const(*i_it).call_function()).get_identifier();
52
53 // see if we have it
54 const namespacet ns(symbol_table);
55 const symbolt &function_symbol=ns.lookup(identifier);
57
59
60 for(std::size_t nr=0; nr<code_type.parameters().size(); nr++)
61 {
62 irep_idt p_identifier=code_type.parameters()[nr].get_identifier();
63
64 if(p_identifier.empty())
65 continue;
66
67 if(nr < as_const(*i_it).call_arguments().size())
68 {
70 symbol_exprt lhs=lhs_symbol.symbol_expr();
72 as_const(*i_it).call_arguments()[nr], lhs.type());
74 code_assignt(lhs, rhs), i_it->source_location()));
75 }
76 }
77
78 std::size_t count=tmp.instructions.size();
79 goto_program.insert_before_swap(i_it, tmp);
80
81 for(; count!=0; count--) i_it++;
82 }
83 }
84}
85
87{
88 for(auto &gf_entry : goto_functions.function_map)
89 do_function_calls(gf_entry.second.body);
90}
91
94 symbol_tablet &symbol_table,
95 goto_functionst &goto_functions)
96{
97 parameter_assignmentst rr(symbol_table);
98 rr(goto_functions);
99}
100
103{
105 rr(goto_model.goto_functions);
106}
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A codet representing an assignment in the program.
Base type of functions.
Definition std_types.h:539
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
typet & type()
Return the type of the expression.
Definition expr.h:82
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
A generic container class for the GOTO intermediate representation of one function.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void do_function_calls(goto_programt &goto_program)
turns x=f(...) into f(...); lhs=f::return_value;
void operator()(goto_functionst &goto_functions)
parameter_assignmentst(symbol_tablet &_symbol_table)
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
The symbol table.
Symbol table entry.
Definition symbol.h:28
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:1928
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
void parameter_assignments(symbol_tablet &symbol_table, goto_functionst &goto_functions)
removes returns
Add parameter assignments.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Author: Diffblue Ltd.