Add some further library functions

src/analyses/libraryFunctions.ml

@@ -29,6 +29,19 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("iswalnum", unknown [drop "wc" []]);
     ("iswprint", unknown [drop "wc" []]);
     ("rename" , unknown [drop "oldpath" [r]; drop "newpath" [r];]);
+    ("puts", unknown [drop "s" [r]]);
+    ("strspn", unknown [drop "s" [r]; drop "accept" [r]]);
+    ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]);
+    ("strtod", unknown [drop "nptr" [r]; drop "endptr" [w_deep]]);
+    ("strtol", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]);
+    ("strtoll", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]);
+    ("strtoul", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]);
+    ("strtoull", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]);
+    ("mktime", unknown [drop "tm" [r;w]]);
+    ("ctime", unknown [drop "rm" [r]]);
+    ("clearerr", unknown [drop "stream" [w]]);
+    ("setbuf", unknown [drop "stream" [w]; drop "buf" [w]]);
+    ("swprintf", unknown (drop "wcs" [w] :: drop "maxlen" [] :: drop "fmt" [r] :: VarArgs (drop' [])));
   ]
 
 (** C POSIX library functions.
@@ -65,6 +78,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("symlink" , unknown [drop "oldpath" [r]; drop "newpath" [r];]);
     ("ftruncate", unknown [drop "fd" []; drop "length" []]);
     ("mkfifo", unknown [drop "pathname" [r]; drop "mode" []]);
+    ("ntohs", unknown [drop "netshort" []]);
   ]
 
 (** Pthread functions. *)
@@ -75,6 +89,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_cond_broadcast", special [__ "cond" []] @@ fun cond -> Broadcast cond);
     ("pthread_cond_wait", special [__ "cond" []; __ "mutex" []] @@ fun cond mutex -> Wait {cond; mutex});
     ("pthread_cond_timedwait", special [__ "cond" []; __ "mutex" []; __ "abstime" [r]] @@ fun cond mutex abstime -> TimedWait {cond; mutex; abstime});
+    ("pthread_attr_destroy", unknown [drop "attr" [f]])
   ]
 
 (** GCC builtin functions.
@@ -111,6 +126,9 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__builtin_add_overflow_p", unknown [drop "a" []; drop "b" []; drop "c" []]);
     ("__builtin_sub_overflow_p", unknown [drop "a" []; drop "b" []; drop "c" []]);
     ("__builtin_mul_overflow_p", unknown [drop "a" []; drop "b" []; drop "c" []]);
+    ("__builtin_popcount", unknown [drop "x" []]);
+    ("__builtin_popcountl", unknown [drop "x" []]);
+    ("__builtin_popcountll", unknown [drop "x" []]);
   ]
 
 let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -128,6 +146,12 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__overflow", unknown [drop "f" [r]; drop "ch" []]);
     ("__ctype_get_mb_cur_max", unknown []);
     ("__xmknod", unknown [drop "ver" []; drop "path" [r]; drop "mode" []; drop "dev" [r; w]]);
+    ("__bad_percpu_size",  special' [] @@ fun () -> Abort); (* these do not have defintions so the linker will fail if they are actually called *)
+    ("__bad_size_call_parameter",  special' [] @@ fun () -> Abort);
+    ("__xchg_wrong_size",  special' [] @@ fun () -> Abort);
+    ("__cmpxchg_wrong_size",  special' [] @@ fun () -> Abort);
+    ("__xadd_wrong_size",  special' [] @@ fun () -> Abort);
+    ("__put_user_bad",  special' [] @@ fun () -> Abort);
   ]
 
 let big_kernel_lock = AddrOf (Cil.var (Goblintutil.create_var (makeGlobalVar "[big kernel lock]" intType)))
@@ -534,7 +558,6 @@ let invalidate_actions = [
     "getopt_long", writesAllButFirst 2 readsAll;(*drop 2*)
     "__strdup", readsAll;(*safe*)
     "strtoul__extinline", readsAll;(*safe*)
-    "strtol", writes [2];
     "geteuid", readsAll;(*safe*)
     "opendir", readsAll;  (*safe*)
     "readdir_r", writesAll;(*unsafe*)

tests/regression/41-stdlib/04-more.c

@@ -0,0 +1,28 @@
+// PARAM: --set pre.cppflags[+] -DGOBLINT_NO_QSORT
+#include<goblint.h>
+#include <wchar.h>
+#include <stdio.h>
+
+int g = 8;
+
+int main() {
+
+    int r = __builtin_popcount(5u);
+    int r = __builtin_popcountl(5ul);
+    int r = __builtin_popcountll(5ul);
+    puts("blarg");
+
+    int a = strspn("bla","blu");
+    a = strcspn("bla","blu");
+
+    long r =  strtol("bla", 0, 8);
+
+    wchar_t wcsbuf[100];
+    wchar_t wstring[] = L"ABCDE";
+    int     num;
+
+    num = swprintf(wcsbuf, 100, L"%s", "xyz");
+
+    // Should not be invalidated
+    __goblint_check(g == 8);
+}