Skip to content

Commit 38516c3

Browse files
committed
goto-symex can safely propagate with_exprt
We would only deem with_exprt constant when all their operands are constant, which means that the array operand must be an array or array_of expression, and both update indices as well as update values must be constant. In most such cases the simplifier would rewrite the with_exprt anyway. The exception to this is an index that cannot immediately be evaluated to a numeric constant, as is the case with, e.g., pointer_object expressions. Fixes: diffblue#3095
1 parent b55efe9 commit 38516c3

File tree

1 file changed

+0
-15
lines changed

1 file changed

+0
-15
lines changed

src/goto-symex/goto_symex_is_constant.h

Lines changed: 0 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -40,21 +40,6 @@ class goto_symex_is_constantt : public is_constantt
4040

4141
return !found_non_constant;
4242
}
43-
else if(expr.id() == ID_with)
44-
{
45-
// this is bad
46-
#if 0
47-
for(const auto &op : expr.operands())
48-
{
49-
if(!is_constant(op))
50-
return false;
51-
}
52-
53-
return true;
54-
#else
55-
return false;
56-
#endif
57-
}
5843

5944
return is_constantt::is_constant(expr);
6045
}

0 commit comments

Comments
 (0)