Move *_unlocked functions to glibc group, fix *wscanf varargs

goblint · Nov 22, 2023 · c98025c · c98025c
1 parent 949432b
commit c98025c
Showing 1 changed file with 10 additions and 10 deletions.
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
@@ -37,9 +37,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("asctime", unknown ~attrs:[ThreadUnsafe] [drop "time_ptr" [r_deep]]);
     ("fclose", unknown [drop "stream" [r_deep; w_deep; f_deep]]);
     ("feof", unknown [drop "stream" [r_deep; w_deep]]);
-    ("feof_unlocked", unknown [drop "stream" [r_deep; w_deep]]);
     ("ferror", unknown [drop "stream" [r_deep; w_deep]]);
-    ("ferror_unlocked", unknown [drop "stream" [r_deep; w_deep]]);
     ("fflush", unknown [drop "stream" [r_deep; w_deep]]);
     ("fgetc", unknown [drop "stream" [r_deep; w_deep]]);
     ("getc", unknown [drop "stream" [r_deep; w_deep]]);
@@ -54,11 +52,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("putc", unknown [drop "ch" []; drop "stream" [r_deep; w_deep]]);
     ("fputs", unknown [drop "str" [r]; drop "stream" [r_deep; w_deep]]);
     ("fread", unknown [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
-    ("__fread_chk_warn", unknown [drop "buffer" [w]; drop "os" []; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
     ("fseek", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "origin" []]);
     ("ftell", unknown [drop "stream" [r_deep]]);
     ("fwrite", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
-    ("fwrite_unlocked", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
     ("rewind", unknown [drop "stream" [r_deep; w_deep]]);
     ("setvbuf", unknown [drop "stream" [r_deep; w_deep]; drop "buffer" [r; w]; drop "mode" []; drop "size" []]);
     (* TODO: if this is used to set an input buffer, the buffer (second argument) would need to remain TOP, *)
@@ -123,11 +119,10 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("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]]);
-    ("clearerr_unlocked", unknown [drop "stream" [w]]);
+    ("clearerr", unknown [drop "stream" [w]]); (* TODO: why only w? *)
     ("setbuf", unknown [drop "stream" [w]; drop "buf" [w]]);
     ("wprintf", unknown (drop "fmt" [r] :: VarArgs (drop' [r])));
-    ("fwprintf", unknown (drop "stream" [w] :: drop "fmt" [r] :: VarArgs (drop' [r])));
+    ("fwprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "fmt" [r] :: VarArgs (drop' [r])));
     ("swprintf", unknown (drop "wcs" [w] :: drop "maxlen" [] :: drop "fmt" [r] :: VarArgs (drop' [r])));
     ("assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" }); (* only used if assert is used without include, e.g. in transformed files *)
     ("difftime", unknown [drop "time1" []; drop "time2" []]);
@@ -161,9 +156,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]);
     ("_Exit", special [drop "status" []] @@ Abort);
     ("strcoll", unknown [drop "lhs" [r]; drop "rhs" [r]]);
-    ("wscanf", unknown (drop "fmt" [r] :: VarArgs (drop' [r])));
-    ("fwscanf", unknown (drop "stream" [r] :: drop "fmt" [r] :: VarArgs (drop' [r])));
-    ("swscanf", unknown (drop "buffer" [r] :: drop "fmt" [r] :: VarArgs (drop' [r])));
+    ("wscanf", unknown (drop "fmt" [r] :: VarArgs (drop' [w])));
+    ("fwscanf", unknown (drop "stream" [r_deep; w_deep] :: drop "fmt" [r] :: VarArgs (drop' [w])));
+    ("swscanf", unknown (drop "buffer" [r] :: drop "fmt" [r] :: VarArgs (drop' [w])));
   ]
 
 (** C POSIX library functions.
@@ -586,6 +581,10 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
 
 let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("fputs_unlocked", unknown [drop "s" [r]; drop "stream" [w]]);
+    ("feof_unlocked", unknown [drop "stream" [r_deep; w_deep]]);
+    ("ferror_unlocked", unknown [drop "stream" [r_deep; w_deep]]);
+    ("fwrite_unlocked", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
+    ("clearerr_unlocked", unknown [drop "stream" [w]]); (* TODO: why only w? *)
     ("futimesat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "times" [r]]);
     ("error", unknown ((drop "status" []) :: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r]))));
     ("warn", unknown (drop "format" [r] :: VarArgs (drop' [r])));
@@ -597,6 +596,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__fgets_chk", unknown [drop "__s" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
     ("__fread_alias", unknown [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
     ("__fread_chk", unknown [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
+    ("__fread_chk_warn", unknown [drop "buffer" [w]; drop "os" []; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
     ("fread_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
     ("__fread_unlocked_alias", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
     ("__fread_unlocked_chk", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);