Skip to content

Commit d3ee1ab

Browse files
authored
Merge pull request #6382 from diffblue/interpreter_evaluate
change signature of interpretert::evaluate
2 parents b95e229 + 43ca425 commit d3ee1ab

File tree

5 files changed

+147
-218
lines changed

5 files changed

+147
-218
lines changed

src/goto-instrument/contracts/assigns.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ static const slicet normalize_to_slice(const exprt &expr, const namespacet &ns)
3333
pointer_offset(arg)},
3434
typecast_exprt::conditional_cast(object_size(arg), signed_size_type())};
3535
}
36-
else if(is_lvalue(expr))
36+
else if(is_assignable(expr))
3737
{
3838
const auto &size = size_of_expr(expr.type(), ns);
3939

src/goto-programs/interpreter.cpp

Lines changed: 10 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -298,8 +298,7 @@ void interpretert::step()
298298

299299
if(call_stack.top().return_value_address != 0)
300300
{
301-
mp_vectort rhs;
302-
evaluate(pc->return_value(), rhs);
301+
mp_vectort rhs = evaluate(pc->return_value());
303302
assign(call_stack.top().return_value_address, rhs);
304303
}
305304

@@ -390,15 +389,14 @@ void interpretert::execute_other()
390389
DATA_INVARIANT(
391390
pc->get_code().operands().size() == 1,
392391
"expression statement expected to have one operand");
393-
mp_vectort rhs;
394-
evaluate(pc->get_code().op0(), rhs);
392+
mp_vectort rhs = evaluate(pc->get_code().op0());
395393
}
396394
else if(statement==ID_array_set)
397395
{
398-
mp_vectort tmp, rhs;
399-
evaluate(pc->get_code().op1(), tmp);
396+
mp_vectort tmp = evaluate(pc->get_code().op1());
400397
mp_integer address = evaluate_address(pc->get_code().op0());
401398
mp_integer size = get_size(pc->get_code().op0().type());
399+
mp_vectort rhs;
402400
while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
403401
if(size!=rhs.size())
404402
output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
@@ -656,8 +654,7 @@ void interpretert::execute_assign()
656654
const exprt &assign_lhs = pc->assign_lhs();
657655
const exprt &assign_rhs = pc->assign_rhs();
658656

659-
mp_vectort rhs;
660-
evaluate(assign_rhs, rhs);
657+
mp_vectort rhs = evaluate(assign_rhs);
661658

662659
if(!rhs.empty())
663660
{
@@ -780,7 +777,7 @@ void interpretert::execute_function_call()
780777
argument_values.resize(call_arguments.size());
781778

782779
for(std::size_t i = 0; i < call_arguments.size(); i++)
783-
evaluate(call_arguments[i], argument_values[i]);
780+
argument_values[i] = evaluate(call_arguments[i]);
784781

785782
// do the call
786783

@@ -827,10 +824,10 @@ void interpretert::execute_function_call()
827824

828825
if(it!=function_input_vars.end())
829826
{
830-
mp_vectort value;
831827
PRECONDITION(!it->second.empty());
832828
PRECONDITION(!it->second.front().return_assignments.empty());
833-
evaluate(it->second.front().return_assignments.back().value, value);
829+
mp_vectort value =
830+
evaluate(it->second.front().return_assignments.back().value);
834831
if(return_value_address>0)
835832
{
836833
assign(return_value_address, value);
@@ -891,8 +888,7 @@ typet interpretert::concretize_type(const typet &type)
891888
if(type.id()==ID_array)
892889
{
893890
const exprt &size_expr=static_cast<const exprt &>(type.find(ID_size));
894-
mp_vectort computed_size;
895-
evaluate(size_expr, computed_size);
891+
mp_vectort computed_size = evaluate(size_expr);
896892
if(computed_size.size()==1 &&
897893
computed_size[0]>=0)
898894
{
@@ -1013,8 +1009,7 @@ mp_integer interpretert::get_size(const typet &type)
10131009

10141010
mp_integer subtype_size=get_size(type.subtype());
10151011

1016-
mp_vectort i;
1017-
evaluate(size_expr, i);
1012+
mp_vectort i = evaluate(size_expr);
10181013
if(i.size()==1)
10191014
{
10201015
// Go via the binary representation to reproduce any

src/goto-programs/interpreter_class.h

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -275,8 +275,7 @@ class interpretert
275275

276276
bool evaluate_boolean(const exprt &expr)
277277
{
278-
mp_vectort v;
279-
evaluate(expr, v);
278+
mp_vectort v = evaluate(expr);
280279
if(v.size()!=1)
281280
throw "invalid boolean value";
282281
return v.front()!=0;
@@ -296,9 +295,7 @@ class interpretert
296295
const mp_integer &cell_offset,
297296
mp_integer &result);
298297

299-
void evaluate(
300-
const exprt &expr,
301-
mp_vectort &dest);
298+
mp_vectort evaluate(const exprt &);
302299

303300
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false);
304301

0 commit comments

Comments
 (0)