Make getaddrinfo specification more precise

goblint · Aug 23, 2023 · 5e8e2c7 · 5e8e2c7
1 parent 20b75c6
commit 5e8e2c7
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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
@@ -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. *)