diff --git a/CHANGELOG.md b/CHANGELOG.md index b7c00ea686..ed5dccdd8b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,6 @@ +## v2.7.1 Bamboozled Buffalo +* Add library function specifications for fortified `inet_pton` and `inet_ntop` (#1883). + ## v2.7.0 Bamboozled Buffalo Functionally equivalent to Goblint in SV-COMP 2026. diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 8f7c175ffe..ee663d4152 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -354,7 +354,13 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pclose", unknown [drop "stream" [w; f]]); ("getcwd", unknown [drop "buf" [w]; drop "size" []]); ("inet_pton", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]]); + ("__inet_pton_alias", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]]); + ("__inet_pton_chk", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]; drop "os" []]); + ("__inet_pton_chk_warn", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]; drop "os" []]); ("inet_ntop", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]; drop "size" []]); + ("__inet_ntop_alias", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]; drop "size" []]); + ("__inet_ntop_chk", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]; drop "size" []; drop "os" []]); + ("__inet_ntop_chk_warn", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]; drop "size" []; drop "os" []]); ("gethostent", unknown ~attrs:[ThreadUnsafe] []); ("poll", unknown [drop "fds" [r]; drop "nfds" []; drop "timeout" []]); ("semget", unknown [drop "key" []; drop "nsems" []; drop "semflg" []]);