Fix ReachableFrom precision loss with int argument in 68-longjmp/41-p…

…oison-rec
goblint · Sep 19, 2023 · 204594e · 204594e
1 parent c458db2
commit 204594e
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -1293,7 +1293,12 @@ struct
             AD.add UnknownPtr addrs' (* add unknown back *)
           else
             addrs'
-        | Int i -> AD.of_int i
+        | Int i ->
+          begin match Cilfacade.typeOf e with
+            | t when Cil.isPointerType t -> AD.of_int i (* integer used as pointer *)
+            | _
+            | exception Cilfacade.TypeOfError _ -> AD.empty () (* avoid unknown pointer result for non-pointer expression *)
+          end
         | _ -> AD.empty ()
       end
     | Q.ReachableUkTypes e -> begin