Be more conservative for ioctl

michael-schwarz · michael-schwarz · commit ea83c30f1db5 · 2023-12-13T16:11:38.000+01:00
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
@@ -750,7 +750,7 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size);
     ("kzalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Calloc {count = Cil.one; size});
     ("usb_alloc_urb", special [__ "iso_packets" []; drop "mem_flags" []] @@ fun iso_packets -> Malloc MyCFG.unknown_exp);
-    ("ioctl", unknown (drop "fd" [] :: drop "request" [] :: VarArgs (drop' [r])));
+    ("ioctl", unknown (drop "fd" [] :: drop "request" [] :: VarArgs (drop' [r_deep; w_deep])));
   ]
 
 (** Goblint functions. *)

Original file line number	Diff line number	Diff line change
`@@ -750,7 +750,7 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[`
`750`	`750`	`("__kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size);`
`751`	`751`	`("kzalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Calloc {count = Cil.one; size});`
`752`	`752`	`("usb_alloc_urb", special [__ "iso_packets" []; drop "mem_flags" []] @@ fun iso_packets -> Malloc MyCFG.unknown_exp);`
`753`		`- ("ioctl", unknown (drop "fd" [] :: drop "request" [] :: VarArgs (drop' [r])));`
	`753`	`+ ("ioctl", unknown (drop "fd" [] :: drop "request" [] :: VarArgs (drop' [r_deep; w_deep])));`
`754`	`754`	`]`
`755`	`755`
`756`	`756`	`(** Goblint functions. *)`