Merge pull request #1167 from goblint/libfuns-zlib-lzma

Add `zlib` and `liblzma` functions used in `The Silver Searcher` to `LibraryFunctions`
goblint · Sep 18, 2023 · 4c9904a · 4c9904a
2 parents 1feb75e + 684cfa8
commit 4c9904a
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 2 deletions.
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
@@ -102,6 +102,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("vprintf", unknown [drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vfprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vsprintf", unknown [drop "buffer" [w]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
+    ("vasprintf", unknown [drop "strp" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
+    ("vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("mktime", unknown [drop "tm" [r;w]]);
     ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]);
     ("clearerr", unknown [drop "stream" [w]]);
@@ -288,6 +290,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("ftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []]); (* TODO: use Call instead of Spawn *)
     ("nftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []; drop "flags" []]); (* TODO: use Call instead of Spawn *)
     ("fnmatch", unknown [drop "pattern" [r]; drop "string" [r]; drop "flags" []]);
+    ("realpath", unknown [drop "path" [r]; drop "resolved_path" [w]]);
   ]
 
 (** Pthread functions. *)
@@ -824,6 +827,19 @@ let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pcre_version", unknown []);
   ]
 
+let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("inflate", unknown [drop "strm" [r_deep; w_deep]; drop "flush" []]);
+    ("inflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []]);
+    ("inflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []; drop "version" [r]; drop "stream_size" []]);
+    ("inflateEnd", unknown [drop "strm" [f_deep]]);
+  ]
+
+let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("lzma_code", unknown [drop "strm" [r_deep; w_deep]; drop "action" []]);
+    ("lzma_auto_decoder", unknown [drop "strm" [r_deep; w_deep]; drop "memlimit" []; drop "flags" []]);
+    ("lzma_end", unknown [drop "strm" [r_deep; w_deep; f_deep]]);
+  ]
+
 let libraries = Hashtbl.of_list [
     ("c", c_descs_list @ math_descs_list);
     ("posix", posix_descs_list);
@@ -837,6 +853,8 @@ let libraries = Hashtbl.of_list [
     ("ncurses", ncurses_descs_list);
     ("zstd", zstd_descs_list);
     ("pcre", pcre_descs_list);
+    ("zlib", zlib_descs_list);
+    ("liblzma", liblzma_descs_list);
   ]
 
 let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t =
@@ -1071,7 +1089,6 @@ let invalidate_actions = [
     "usleep", readsAll;
     "svc_run", writesAll;(*unsafe*)
     "dup", readsAll; (*safe*)
-    "vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
     "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
     "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*)
     "strcasecmp", readsAll; (*safe*)

diff --git a/src/util/options.schema.json b/src/util/options.schema.json
@@ -1285,7 +1285,9 @@
               "sv-comp",
               "ncurses",
               "zstd",
-              "pcre"
+              "pcre",
+              "zlib",
+              "liblzma"
             ]
           },
           "default": [