cprover
Loading...
Searching...
No Matches
goto_convert_function_call.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "goto_convert_class.h"
13
14#include <util/expr_util.h>
16#include <util/std_expr.h>
17
19 const code_function_callt &function_call,
20 goto_programt &dest,
21 const irep_idt &mode)
22{
24 function_call.lhs(),
25 function_call.function(),
26 function_call.arguments(),
27 dest,
28 mode);
29}
30
32 const exprt &lhs,
33 const exprt &function,
34 const exprt::operandst &arguments,
35 goto_programt &dest,
36 const irep_idt &mode)
37{
38 // make it all side effect free
39
40 exprt new_lhs=lhs,
41 new_function=function;
42
44
45 if(!new_lhs.is_nil())
46 clean_expr(new_lhs, dest, mode);
47
48 clean_expr(new_function, dest, mode);
49
50 for(auto &new_argument : new_arguments)
51 clean_expr(new_argument, dest, mode);
52
53 // split on the function
54
55 if(new_function.id()==ID_if)
56 {
59 }
60 else if(new_function.id()==ID_symbol)
61 {
64 }
65 else if(new_function.id() == ID_null_object)
66 {
67 }
68 else if(new_function.id()==ID_dereference ||
69 new_function.id()=="virtual_function")
70 {
72 }
73 else
74 {
76 false,
77 "unexpected function argument",
78 new_function.id(),
79 function.find_source_location());
80 }
81}
82
84 const exprt &lhs,
85 const if_exprt &function,
86 const exprt::operandst &arguments,
87 goto_programt &dest,
88 const irep_idt &mode)
89{
90 // case split
91
92 // c?f():g()
93 //--------------------
94 // v: if(!c) goto y;
95 // w: f();
96 // x: goto z;
97 // y: g();
98 // z: ;
99
100 // do the v label
103 boolean_negate(function.cond()), function.cond().source_location()));
104
105 // do the x label
109
110 // do the z label
113
114 // y: g();
117
118 do_function_call(lhs, function.false_case(), arguments, tmp_y, mode);
119
120 if(tmp_y.instructions.empty())
122 else
123 y=tmp_y.instructions.begin();
124
125 // v: if(!c) goto y;
126 v->complete_goto(y);
127
128 // w: f();
130
131 do_function_call(lhs, function.true_case(), arguments, tmp_w, mode);
132
133 if(tmp_w.instructions.empty())
135
136 // x: goto z;
137 x->complete_goto(z);
138
144}
145
147 const exprt &lhs,
148 const exprt &function,
149 const exprt::operandst &arguments,
150 goto_programt &dest)
151{
152 // don't know what to do with it
153 code_function_callt function_call(lhs, function, arguments);
154 function_call.add_source_location()=function.source_location();
156 function_call, function.source_location()));
157}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
goto_instruction_codet representation of a function call statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
virtual void do_function_call_if(const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
add function calls to function queue for later processing
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
virtual void do_function_call_other(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
Definition std_expr.h:2323
exprt & cond()
Definition std_expr.h:2340
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
The Boolean constant true.
Definition std_expr.h:3008
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
Program Transformation.
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition invariant.h:437
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222