Remove old library function classify

goblint · Sep 18, 2023 · 4e83af9 · 4e83af9
1 parent f27a6e7
commit 4e83af9
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 51 deletions.
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
@@ -126,31 +126,10 @@ type t = {
   attrs: attr list; (** Attributes of function. *)
 }
 
-let special_of_old classify_name = fun args ->
-  match classify_name args with
-  | `Malloc e -> Malloc e
-  | `Calloc (count, size) -> Calloc { count; size; }
-  | `Realloc (ptr, size) -> Realloc { ptr; size; }
-  | `Lock (try_, write, return_on_success) ->
-    begin match args with
-      | [lock] -> Lock { lock ; try_; write; return_on_success; }
-      | [] -> failwith "lock has no arguments"
-      | _ -> failwith "lock has multiple arguments"
-    end
-  | `Unlock ->
-    begin match args with
-      | [arg] -> Unlock arg
-      | [] -> failwith "unlock has no arguments"
-      | _ -> failwith "unlock has multiple arguments"
-    end
-  | `ThreadCreate (thread, start_routine, arg) -> ThreadCreate { thread; start_routine; arg; }
-  | `ThreadJoin (thread, ret_var) -> ThreadJoin { thread; ret_var; }
-  | `Unknown _ -> Unknown
-
-let of_old ?(attrs: attr list=[]) (old_accesses: Accesses.old) (classify_name): t = {
+let of_old ?(attrs: attr list=[]) (old_accesses: Accesses.old): t = {
   attrs;
   accs = Accesses.of_old old_accesses;
-  special = special_of_old classify_name;
+  special = fun _ -> Unknown;
 }
 
 module MathPrintable = struct

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
@@ -918,21 +918,6 @@ let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t
 let reset_lazy () =
   ResettableLazy.reset activated_library_descs
 
-type categories = [
-  | `Malloc       of exp
-  | `Calloc       of exp * exp
-  | `Realloc      of exp * exp
-  | `Lock         of bool * bool * bool  (* try? * write? * return  on success *)
-  | `Unlock
-  | `ThreadCreate of exp * exp * exp (* id * f  * x       *)
-  | `ThreadJoin   of exp * exp (* id * ret_var *)
-  | `Unknown      of string ]
-
-
-let classify fn exps: categories =
-  fn
-
-
 module Invalidate =
 struct
   [@@@warning "-unused-value-declaration"] (* some functions are not used below *)
@@ -1221,7 +1206,7 @@ let is_safe_uncalled fn_name =
   List.exists (fun r -> Str.string_match r fn_name 0) kernel_safe_uncalled_regex
 
 
-let unknown_desc ~f name = (* TODO: remove name argument, unknown function shouldn't have classify *)
+let unknown_desc f =
   let old_accesses (kind: AccessKind.t) args = match kind with
     | Write when GobConfig.get_bool "sem.unknown_function.invalidate.args" -> args
     | Write -> []
@@ -1239,16 +1224,10 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul
     else
       []
   in
-  let classify_name args =
-    match classify name args with
-    | `Unknown _ as category ->
-      (* TODO: remove hack when all classify are migrated *)
-      if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then
-        M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname;
-      category
-    | category -> category
-  in
-  LibraryDesc.of_old ~attrs old_accesses classify_name
+  (* TODO: remove hack when all classify are migrated *)
+  if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then
+    M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname;
+  LibraryDesc.of_old ~attrs old_accesses
 
 let find f =
   let name = f.vname in
@@ -1257,9 +1236,9 @@ let find f =
   | None ->
     match get_invalidate_action name with
     | Some old_accesses ->
-      LibraryDesc.of_old old_accesses (classify name)
+      LibraryDesc.of_old old_accesses
     | None ->
-      unknown_desc ~f name
+      unknown_desc f
 
 
 let is_special fv =