diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index d9211ce897..67ba8c8c20 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -279,7 +279,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env }); (* has two underscores *) ("sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env }); ("siglongjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value }); - ("getaddrinfo", unknown [drop "node" [r]; drop "service" [r]; drop "hints" [r_deep]; drop "res" [w_deep]]); + ("getaddrinfo", unknown [drop "node" [r]; drop "service" [r]; drop "hints" [r_deep]; drop "res" [w]]); (* only write res non-deep because it doesn't write to existing fields of res *) ] (** Pthread functions. *) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 71ab214481..811d1afffc 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -455,6 +455,7 @@ struct let remove_reachable ~deep ask es st = let rs = reachables ~deep ask es in + if M.tracing then M.tracel "var_eq" "remove_reachable %a: %a\n" (Pretty.d_list ", " d_exp) es AD.pretty rs; (* Prior to https://github.com/goblint/analyzer/pull/694 checks were done "in the other direction": each expression in st was checked for reachability from es/rs using very conservative but also unsound reachable_from. It is unknown, why that was necessary. *)