From 7159875257d594d248b3b3b7b0560e4c37e91f09 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 22 Nov 2023 13:47:15 +0200 Subject: [PATCH] Add fun defs for wprintf, iswxdigit and .*wscanf #1239 --- src/analyses/libraryFunctions.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 1a032c84b3..20995e2f09 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -125,6 +125,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("clearerr", unknown [drop "stream" [w]]); ("clearerr_unlocked", unknown [drop "stream" [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]))); ("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" []]); @@ -158,6 +160,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]))); ] (** C POSIX library functions.