From 204594e695c92d106e6e9e628109228f20712339 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 19 Sep 2023 17:45:22 +0300 Subject: [PATCH] Fix ReachableFrom precision loss with int argument in 68-longjmp/41-poison-rec --- src/analyses/base.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 4e7235de2b..0e6ad8f516 100644 --- 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