Fix LibraryFunctions.invalidate_actions indentation

goblint · Dec 7, 2023 · 5662024 · 5662024
1 parent 9261b71
commit 5662024
Showing 1 changed file with 82 additions and 82 deletions.
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
@@ -1233,88 +1233,88 @@ open Invalidate
  * We assume that no known functions that are reachable are executed/spawned. For that we use ThreadCreate above. *)
 (* WTF: why are argument numbers 1-indexed (in partition)? *)
 let invalidate_actions = [
-    "__printf_chk", readsAll;(*safe*)
-    "printk", readsAll;(*safe*)
-    "__mutex_init", readsAll;(*safe*)
-    "__builtin___snprintf_chk", writes [1];(*keep [1]*)
-    "__vfprintf_chk", writes [1];(*keep [1]*)
-    "__builtin_va_arg", readsAll;(*safe*)
-    "__builtin_va_end", readsAll;(*safe*)
-    "__builtin_va_start", readsAll;(*safe*)
-    "__ctype_b_loc", readsAll;(*safe*)
-    "__errno", readsAll;(*safe*)
-    "__errno_location", readsAll;(*safe*)
-    "__strdup", readsAll;(*safe*)
-    "strtoul__extinline", readsAll;(*safe*)
-    "readdir_r", writesAll;(*unsafe*)
-    "atoi__extinline", readsAll;(*safe*)
-    "_IO_getc", writesAll;(*unsafe*)
-    "pipe", writesAll;(*unsafe*)
-    "strerror_r", writesAll;(*unsafe*)
-    "raise", writesAll;(*unsafe*)
-    "_strlen", readsAll;(*safe*)
-    "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
-    "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
-    "waitpid", readsAll;(*safe*)
-    "__open_alias", readsAll;(*safe*)
-    "__open_2", readsAll;(*safe*)
-    "ioctl", writesAll;(*unsafe*)
-    "fstat__extinline", writesAll;(*unsafe*)
-    "scandir", writes [1;3;4];(*keep [1;3;4]*)
-    "bindtextdomain", readsAll;(*safe*)
-    "textdomain", readsAll;(*safe*)
-    "dcgettext", readsAll;(*safe*)
-    "putw", readsAll;(*safe*)
-    "__getdelim", writes [3];(*keep [3]*)
-    "__h_errno_location", readsAll;(*safe*)
-    "__fxstat", readsAll;(*safe*)
-    "openlog", readsAll;(*safe*)
-    "umask", readsAll;(*safe*)
-    "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*)
-    "svctcp_create", readsAll;(*safe*)
-    "clntudp_bufcreate", writesAll;(*unsafe*)
-    "authunix_create_default", readsAll;(*safe*)
-    "clnt_broadcast", writesAll;(*unsafe*)
-    "clnt_sperrno", readsAll;(*safe*)
-    "pmap_unset", writesAll;(*unsafe*)
-    "svcudp_create", readsAll;(*safe*)
-    "svc_register", writesAll;(*unsafe*)
-    "svc_run", writesAll;(*unsafe*)
-    "dup", readsAll; (*safe*)
-    "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
-    "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*)
-    "__error", readsAll; (*safe*)
-    "__maskrune", writesAll; (*unsafe*)
-    "times", writesAll; (*unsafe*)
-    "timespec_get", writes [1];
-    "__tolower", readsAll; (*safe*)
-    "signal", writesAll; (*unsafe*)
-    "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*)
-    "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*)
-    "uncompress", writes [3;4]; (*keep [3;4]*)
-    "__xstat", writes [3]; (*keep [1]*)
-    "__lxstat", writes [3]; (*keep [1]*)
-    "remove", readsAll;
-    "BZ2_bzBuffToBuffCompress", writes [3;4]; (*keep [3;4]*)
-    "compress2", writes [3]; (*keep [3]*)
-    "__toupper", readsAll; (*safe*)
-    "BF_set_key", writes [3]; (*keep [3]*)
-    "PL_NewHashTable", readsAll; (*safe*)
-    "assert_failed", readsAll; (*safe*)
-    "munmap", readsAll;(*safe*)
-    "mmap", readsAll;(*safe*)
-    "__builtin_va_arg_pack_len", readsAll;
-    "__open_too_many_args", readsAll;
-    "usb_submit_urb", readsAll; (* first argument is written to but according to specification must not be read from anymore *)
-    "dev_driver_string", readsAll;
-    "__spin_lock_init", writes [1];
-    "kmem_cache_create", readsAll;
-    "idr_pre_get", readsAll;
-    "zil_replay", writes [1;2;3;5];
-    (* ddverify *)
-    "sema_init", readsAll;
-    "__goblint_assume_join", readsAll;
-  ]
+  "__printf_chk", readsAll;(*safe*)
+  "printk", readsAll;(*safe*)
+  "__mutex_init", readsAll;(*safe*)
+  "__builtin___snprintf_chk", writes [1];(*keep [1]*)
+  "__vfprintf_chk", writes [1];(*keep [1]*)
+  "__builtin_va_arg", readsAll;(*safe*)
+  "__builtin_va_end", readsAll;(*safe*)
+  "__builtin_va_start", readsAll;(*safe*)
+  "__ctype_b_loc", readsAll;(*safe*)
+  "__errno", readsAll;(*safe*)
+  "__errno_location", readsAll;(*safe*)
+  "__strdup", readsAll;(*safe*)
+  "strtoul__extinline", readsAll;(*safe*)
+  "readdir_r", writesAll;(*unsafe*)
+  "atoi__extinline", readsAll;(*safe*)
+  "_IO_getc", writesAll;(*unsafe*)
+  "pipe", writesAll;(*unsafe*)
+  "strerror_r", writesAll;(*unsafe*)
+  "raise", writesAll;(*unsafe*)
+  "_strlen", readsAll;(*safe*)
+  "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
+  "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
+  "waitpid", readsAll;(*safe*)
+  "__open_alias", readsAll;(*safe*)
+  "__open_2", readsAll;(*safe*)
+  "ioctl", writesAll;(*unsafe*)
+  "fstat__extinline", writesAll;(*unsafe*)
+  "scandir", writes [1;3;4];(*keep [1;3;4]*)
+  "bindtextdomain", readsAll;(*safe*)
+  "textdomain", readsAll;(*safe*)
+  "dcgettext", readsAll;(*safe*)
+  "putw", readsAll;(*safe*)
+  "__getdelim", writes [3];(*keep [3]*)
+  "__h_errno_location", readsAll;(*safe*)
+  "__fxstat", readsAll;(*safe*)
+  "openlog", readsAll;(*safe*)
+  "umask", readsAll;(*safe*)
+  "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*)
+  "svctcp_create", readsAll;(*safe*)
+  "clntudp_bufcreate", writesAll;(*unsafe*)
+  "authunix_create_default", readsAll;(*safe*)
+  "clnt_broadcast", writesAll;(*unsafe*)
+  "clnt_sperrno", readsAll;(*safe*)
+  "pmap_unset", writesAll;(*unsafe*)
+  "svcudp_create", readsAll;(*safe*)
+  "svc_register", writesAll;(*unsafe*)
+  "svc_run", writesAll;(*unsafe*)
+  "dup", readsAll; (*safe*)
+  "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
+  "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*)
+  "__error", readsAll; (*safe*)
+  "__maskrune", writesAll; (*unsafe*)
+  "times", writesAll; (*unsafe*)
+  "timespec_get", writes [1];
+  "__tolower", readsAll; (*safe*)
+  "signal", writesAll; (*unsafe*)
+  "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*)
+  "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*)
+  "uncompress", writes [3;4]; (*keep [3;4]*)
+  "__xstat", writes [3]; (*keep [1]*)
+  "__lxstat", writes [3]; (*keep [1]*)
+  "remove", readsAll;
+  "BZ2_bzBuffToBuffCompress", writes [3;4]; (*keep [3;4]*)
+  "compress2", writes [3]; (*keep [3]*)
+  "__toupper", readsAll; (*safe*)
+  "BF_set_key", writes [3]; (*keep [3]*)
+  "PL_NewHashTable", readsAll; (*safe*)
+  "assert_failed", readsAll; (*safe*)
+  "munmap", readsAll;(*safe*)
+  "mmap", readsAll;(*safe*)
+  "__builtin_va_arg_pack_len", readsAll;
+  "__open_too_many_args", readsAll;
+  "usb_submit_urb", readsAll; (* first argument is written to but according to specification must not be read from anymore *)
+  "dev_driver_string", readsAll;
+  "__spin_lock_init", writes [1];
+  "kmem_cache_create", readsAll;
+  "idr_pre_get", readsAll;
+  "zil_replay", writes [1;2;3;5];
+  (* ddverify *)
+  "sema_init", readsAll;
+  "__goblint_assume_join", readsAll;
+]
 
 let invalidate_actions =
   let tbl = Hashtbl.create 113 in