Skip to content

Commit ff1f4b0

Browse files
author
Thomas Kiley
committed
Ensure void* pointers instructed to be arrays are null-initalized
The current behaviour trips over an invariant. This is the only sesnible behaviour, as cannot sensibly malloc an array of void
1 parent 33294f6 commit ff1f4b0

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/goto-harness/recursive_initialization.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -793,6 +793,15 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor(
793793
PRECONDITION(pointer_type.id() == ID_pointer);
794794
const typet &element_type = pointer_type.subtype();
795795

796+
null_pointer_exprt nullptr_expr{::pointer_type(element_type)};
797+
const code_assignt assign_null{dereference_exprt{result}, nullptr_expr};
798+
799+
// always initalize void* pointers as NULL
800+
if(element_type.id() == ID_empty)
801+
{
802+
return code_blockt{{assign_null, code_returnt{}}};
803+
}
804+
796805
// builds:
797806
// void type_constructor_ptr_T(int depth, T** result, int* size)
798807
// {

0 commit comments

Comments
 (0)