diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index a9cce50b60..8152e5b886 100644 --- 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]]);