CBMC
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
18#include "goto_model.h"
19
21{
22public:
27
28 void operator()(
29 goto_functionst &goto_functions);
30
31protected:
33
35 goto_programt &goto_program);
36};
37
40 goto_programt &goto_program)
41{
43 {
44 if(i_it->is_function_call())
45 {
46 // add x=y for f(y) where x is the parameter
47 PRECONDITION(as_const(*i_it).call_function().id() == ID_symbol);
48
49 const irep_idt &identifier =
50 to_symbol_expr(as_const(*i_it).call_function()).get_identifier();
51
52 // see if we have it
53 const namespacet ns(symbol_table);
54 const symbolt &function_symbol=ns.lookup(identifier);
56
58
59 for(std::size_t nr=0; nr<code_type.parameters().size(); nr++)
60 {
61 irep_idt p_identifier=code_type.parameters()[nr].get_identifier();
62
63 if(p_identifier.empty())
64 continue;
65
66 if(nr < as_const(*i_it).call_arguments().size())
67 {
69 symbol_exprt lhs=lhs_symbol.symbol_expr();
71 as_const(*i_it).call_arguments()[nr], lhs.type());
73 code_assignt(lhs, rhs), i_it->source_location()));
74 }
75 }
76
77 std::size_t count=tmp.instructions.size();
78 goto_program.insert_before_swap(i_it, tmp);
79
80 for(; count!=0; count--) i_it++;
81 }
82 }
83}
84
86{
87 for(auto &gf_entry : goto_functions.function_map)
88 do_function_calls(gf_entry.second.body);
89}
90
93 symbol_table_baset &symbol_table,
94 goto_functionst &goto_functions)
95{
96 parameter_assignmentst rr(symbol_table);
97 rr(goto_functions);
98}
99
102{
104 rr(goto_model.goto_functions);
105}
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:562
A goto_instruction_codet representing an assignment in the program.
Base type of functions.
Definition std_types.h:583
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
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;
parameter_assignmentst(symbol_table_baset &_symbol_table)
void operator()(goto_functionst &goto_functions)
symbol_table_baset & symbol_table
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
void parameter_assignments(symbol_table_baset &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:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788