fix a bug with inclusion checking on havoc_object

The write set inclusion check on havoc_object(ptr) only checked the
inclusion of (ptr+0) in the write set, but performed havocing of the
entire object (i.e., ptr+0 until ptr+OBJECT_SIZE(ptr)).
The proposed change fixes this behavior and checks the inclusion of the
entire object in the write set.

Author: SaswatPadhi

regression/contracts/assigns_enforce_20/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^\[foo.\d+\] line \d+ Check that \*y is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --

src/goto-instrument/contracts/contracts.cpp

@@ -942,8 +942,8 @@ void code_contractst::check_frame_conditions(
       instruction_it->is_other() &&
       instruction_it->get_other().get_statement() == ID_havoc_object)
     {
-      const exprt &havoc_argument = dereference_exprt(
-        to_typecast_expr(instruction_it->get_other().operands().front()).op());
+      const auto havoc_argument =
+        pointer_object(instruction_it->get_other().operands().front());
       add_inclusion_check(body, assigns, instruction_it, havoc_argument);
     }
   }