Skip to content

Commit a9ed380

Browse files
author
Daniel Kroening
authored
Merge pull request #5011 from diffblue/opX-goto-instrument
fix exprt::opX accesses in goto-instrument
2 parents 115c5f8 + 494728d commit a9ed380

File tree

4 files changed

+33
-29
lines changed

4 files changed

+33
-29
lines changed

src/goto-instrument/accelerate/overflow_instrumenter.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -211,7 +211,7 @@ void overflow_instrumentert::overflow_expr(
211211
expr.id()==ID_mult)
212212
{
213213
// A generic arithmetic operation.
214-
exprt overflow("overflow-" + expr.id_string(), bool_typet());
214+
multi_ary_exprt overflow("overflow-" + expr.id_string(), bool_typet());
215215
overflow.operands()=expr.operands();
216216

217217
if(expr.operands().size()>=3)
@@ -223,7 +223,7 @@ void overflow_instrumentert::overflow_expr(
223223

224224
if(i==1)
225225
{
226-
tmp=expr.op0();
226+
tmp = to_multi_ary_expr(expr).op0();
227227
}
228228
else
229229
{

src/goto-instrument/accelerate/polynomial.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -117,10 +117,11 @@ void polynomialt::from_expr(const exprt &expr)
117117
expr.id()==ID_minus ||
118118
expr.id()==ID_mult)
119119
{
120+
const auto &multi_ary_expr = to_multi_ary_expr(expr);
120121
polynomialt poly2;
121122

122-
from_expr(expr.op0());
123-
poly2.from_expr(expr.op1());
123+
from_expr(multi_ary_expr.op0());
124+
poly2.from_expr(multi_ary_expr.op1());
124125

125126
if(expr.id()==ID_minus)
126127
{
@@ -148,7 +149,7 @@ void polynomialt::from_expr(const exprt &expr)
148149
// Pretty shady... We just throw away the typecast... Pretty sure this
149150
// isn't sound.
150151
// XXX - probably not sound.
151-
from_expr(expr.op0());
152+
from_expr(to_typecast_expr(expr).op());
152153
}
153154
else
154155
{

src/goto-instrument/dot.cpp

+23-20
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ class dott
4141

4242
unsigned subgraphscount;
4343

44-
std::list<exprt> function_calls;
44+
std::list<std::pair<std::string, exprt>> function_calls;
4545
std::list<exprt> clusters;
4646

4747
void
@@ -145,17 +145,16 @@ void dott::write_dot_subgraph(
145145
tmp.str("Atomic End");
146146
else if(it->is_function_call())
147147
{
148-
std::string t = from_expr(ns, function_id, it->code);
148+
const auto &function_call = it->get_function_call();
149+
std::string t = from_expr(ns, function_id, function_call);
149150
while(t[ t.size()-1 ]=='\n')
150151
t = t.substr(0, t.size()-1);
151152
tmp.str(escape(t));
152153

153-
exprt fc;
154154
std::stringstream ss;
155155
ss << "Node_" << subgraphscount << "_" << it->location_number;
156-
fc.operands().push_back(exprt(ss.str()));
157-
fc.operands().push_back(it->code.op1());
158-
function_calls.push_back(fc);
156+
function_calls.push_back(
157+
std::pair<std::string, exprt>(ss.str(), function_call.function()));
159158
}
160159
else if(it->is_assign() ||
161160
it->is_decl() ||
@@ -224,36 +223,40 @@ void dott::write_dot_subgraph(
224223
void dott::do_dot_function_calls(
225224
std::ostream &out)
226225
{
227-
for(const auto &expr : function_calls)
226+
for(const auto &call : function_calls)
228227
{
229228
std::list<exprt>::const_iterator cit=clusters.begin();
230229
for( ; cit!=clusters.end(); cit++)
231-
if(cit->get("name")==expr.op1().get(ID_identifier))
230+
if(cit->get("name") == call.second.get(ID_identifier))
232231
break;
233232

234233
if(cit!=clusters.end())
235234
{
236-
out << expr.op0().id() <<
237-
" -> " "Node_" << cit->get("nr") << "_0" <<
238-
" [lhead=\"cluster_" << expr.op1().get(ID_identifier) << "\"," <<
239-
"color=blue];\n";
235+
out << call.first
236+
<< " -> "
237+
"Node_"
238+
<< cit->get("nr") << "_0"
239+
<< " [lhead=\"cluster_" << call.second.get(ID_identifier) << "\","
240+
<< "color=blue];\n";
240241
}
241242
else
242243
{
243-
out << "subgraph \"cluster_" << expr.op1().get(ID_identifier) <<
244-
"\" {\n";
244+
out << "subgraph \"cluster_" << call.second.get(ID_identifier)
245+
<< "\" {\n";
245246
out << "rank=sink;\n";
246-
out << "label=\"" << expr.op1().get(ID_identifier) << "\";\n";
247+
out << "label=\"" << call.second.get(ID_identifier) << "\";\n";
247248
out << "Node_" << subgraphscount << "_0 " <<
248249
"[shape=Mrecord,fontsize=22,label=\"?\"];\n";
249250
out << "}\n";
250251
clusters.push_back(exprt("cluster"));
251-
clusters.back().set("name", expr.op1().get(ID_identifier));
252+
clusters.back().set("name", call.second.get(ID_identifier));
252253
clusters.back().set("nr", subgraphscount);
253-
out << expr.op0().id() <<
254-
" -> " "Node_" << subgraphscount << "_0" <<
255-
" [lhead=\"cluster_" << expr.op1().get("identifier") << "\"," <<
256-
"color=blue];\n";
254+
out << call.first
255+
<< " -> "
256+
"Node_"
257+
<< subgraphscount << "_0"
258+
<< " [lhead=\"cluster_" << call.second.get("identifier") << "\","
259+
<< "color=blue];\n";
257260
subgraphscount++;
258261
}
259262
}

src/goto-instrument/goto_program2code.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -109,8 +109,7 @@ void goto_program2codet::scan_for_varargs()
109109
r.id() == ID_side_effect &&
110110
to_side_effect_expr(r).get_statement() == ID_va_start)
111111
{
112-
assert(r.has_operands());
113-
va_list_expr.insert(r.op0());
112+
va_list_expr.insert(to_unary_expr(r).op());
114113
}
115114
// try our modelling of va_start
116115
else if(l.type().id()==ID_pointer &&
@@ -315,7 +314,8 @@ goto_programt::const_targett goto_program2codet::convert_assign_varargs(
315314
{
316315
code_function_callt f(
317316
symbol_exprt(ID_va_start, code_typet({}, empty_typet())),
318-
{this_va_list_expr, to_address_of_expr(skip_typecast(r.op0())).object()});
317+
{this_va_list_expr,
318+
to_address_of_expr(skip_typecast(to_unary_expr(r).op())).object()});
319319

320320
dest.add(std::move(f));
321321
}
@@ -865,7 +865,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
865865
// try to figure out whether this was a switch/case
866866
exprt eq_cand=target->guard;
867867
if(eq_cand.id()==ID_or)
868-
eq_cand=eq_cand.op0();
868+
eq_cand = to_or_expr(eq_cand).op0();
869869

870870
if(target->is_backwards_goto() ||
871871
eq_cand.id()!=ID_equal ||

0 commit comments

Comments
 (0)