Skip to content

Commit 380533c

Browse files
committed
Value sets: type casts need not be towards a pointer type
We cannot assume that the expression seen by get_value_set_rec is of pointer type. Therefore, type cast expressions need not be towards a pointer type, and unconditionally trying to take the subtype of the expression type is not safe. On the other hand, any access to NULL_object will be invalid, and fixing NULL_object to be void typed should be safe.
1 parent 2349603 commit 380533c

File tree

1 file changed

+3
-6
lines changed

1 file changed

+3
-6
lines changed

src/pointer-analysis/value_set.cpp

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -586,20 +586,17 @@ void value_sett::get_value_set_rec(
586586

587587
if(op_type.id()==ID_pointer)
588588
{
589-
// pointer-to-pointer -- we just ignore these
589+
// pointer-to-something -- we just ignore the type cast
590590
get_value_set_rec(op, dest, suffix, original_type, ns);
591591
}
592592
else if(op_type.id()==ID_unsignedbv ||
593593
op_type.id()==ID_signedbv)
594594
{
595-
// integer-to-pointer
595+
// integer-to-something
596596

597597
if(op.is_zero())
598598
{
599-
insert(
600-
dest,
601-
exprt(ID_null_object, to_type_with_subtype(expr_type).subtype()),
602-
mp_integer{0});
599+
insert(dest, exprt(ID_null_object, empty_typet{}), mp_integer{0});
603600
}
604601
else
605602
{

0 commit comments

Comments
 (0)