goto-symex constant propagation peculiarities #3095
Labels
Comments
3 tasks
tautschnig
added a commit
to tautschnig/cbmc
that referenced
this issue
May 29, 2023
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
CBMC version: 5.10 a1e86d3
Operating system: any
Exact command line resulting in the issue: n/a
What behaviour did you expect: To understand why constant propagation is restricted as it is
What happened instead: Constant propagation in goto-symex is limited to expressions with ids
ID_typecast,ID_array_of,ID_plus,ID_array,ID_struct,ID_union,ID_byte_update_big_endian,ID_byte_update_little_endian, andID_address_of-- if all operands are constants. FurthermoreID_multis always deemed constant irrespective of its operands, andID_withis never constant. It is not clear why this specific set of operations was chosen, andID_withis explained as "this is bad."The text was updated successfully, but these errors were encountered: