Merge pull request #6164 from padhi-aws-forks/assigns_w_ok_bug_fix

Use correct type for pointer checks in contracts

Author: SaswatPadhi

regression/contracts/assigns_replace_03/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --replace-all-calls-with-contracts
 ^EXIT=0$
@@ -7,7 +7,3 @@ main.c
 --
 --
 This test checks that a havocked variable can be constrained by a function post-condition.
-
-Known Bug:
-Currently, there is a bug when char variables are being passed to
-__CPROVER_w_ok(). See GitHub issue #6106 for further details.

src/goto-instrument/code_contracts.cpp

@@ -1698,7 +1698,7 @@ goto_programt assigns_clauset::havoc_code(
     {
       // create the condition
       exprt condition =
-        not_exprt(w_ok_exprt(target_ptr, from_integer(0, integer_typet())));
+        not_exprt(w_ok_exprt(target_ptr, from_integer(0, unsigned_int_type())));
       havoc_statements.add(goto_programt::make_goto(z, condition, location));
     }
 
@@ -1775,8 +1775,8 @@ exprt assigns_clauset::compatible_expression(
           // target->compatible_expression(*called_target) would not be
           // checked on invalid called_targets.
           current_target_compatible = or_exprt(
-            not_exprt(
-              w_ok_exprt(called_target_ptr, from_integer(0, integer_typet()))),
+            not_exprt(w_ok_exprt(
+              called_target_ptr, from_integer(0, unsigned_int_type()))),
             target->compatible_expression(*called_target));
         }
         else