Skip to content

Commit 19858f9

Browse files
author
Owen Jones
committed
Fix zeroing of arrays in value set analysis
Catch when array_set is used to null-initialise the array.
1 parent 12fd5fe commit 19858f9

File tree

1 file changed

+10
-0
lines changed

1 file changed

+10
-0
lines changed

src/pointer-analysis/value_set.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1662,6 +1662,16 @@ void value_sett::apply_code(
16621662
}
16631663
else if(statement==ID_array_set)
16641664
{
1665+
if(code.operands().size()!=2)
1666+
throw "array_set expected to have two operands";
1667+
1668+
const exprt &data_pointer=code.op0();
1669+
const exprt &zero_element=code.op1();
1670+
1671+
typet element_type=data_pointer.type().subtype();
1672+
const dereference_exprt lhs(data_pointer, element_type);
1673+
1674+
assign(lhs, zero_element, ns, true, false);
16651675
}
16661676
else if(statement==ID_array_copy)
16671677
{

0 commit comments

Comments
 (0)