Skip to content

Commit 6bfaf49

Browse files
committed
Enable the interpreter to deal with inline conditionals on addresses
1 parent eec7efd commit 6bfaf49

File tree

1 file changed

+7
-0
lines changed

1 file changed

+7
-0
lines changed

src/goto-programs/interpreter_evaluate.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -962,6 +962,13 @@ mp_integer interpretert::evaluate_address(const exprt &expr, bool fail_quietly)
962962
}
963963
}
964964
}
965+
else if(expr.id()==ID_if)
966+
{
967+
std::vector<mp_integer> result;
968+
evaluate(expr,result);
969+
if(result.size()==1)
970+
return result[0];
971+
}
965972

966973
if(!fail_quietly)
967974
{

0 commit comments

Comments
 (0)