Merge pull request #1523 from goblint/stdlib-starts_with

Use `String.starts_with` and `ends_with` from `Stdlib`

src/analyses/mutexEventsAnalysis.ml

@@ -5,7 +5,6 @@
 module M = Messages
 module Addr = ValueDomain.Addr
 module LF = LibraryFunctions
-open Batteries
 open GoblintCil
 open Analyses
 open GobConfig
@@ -52,12 +51,12 @@ struct
 
   let return ctx exp fundec : D.t =
     (* deprecated but still valid SV-COMP convention for atomic block *)
-    if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then
+    if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname ~prefix:"__VERIFIER_atomic_" then
       ctx.emit (Events.Unlock (LockDomain.Addr.of_var LF.verifier_atomic_var))
 
   let body ctx f : D.t =
     (* deprecated but still valid SV-COMP convention for atomic block *)
-    if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then
+    if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname ~prefix:"__VERIFIER_atomic_" then
       ctx.emit (Events.Lock (LockDomain.Addr.of_var LF.verifier_atomic_var, true))
 
   let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t =

src/autoTune.ml

@@ -104,7 +104,7 @@ let rec setCongruenceRecursive fd depth neigbourFunction =
          | exception Not_found -> () (* Happens for __goblint_bounded *)
       )
       (FunctionSet.filter (*for extern and builtin functions there is no function definition in CIL*)
-         (fun x -> not (isExtern x.vstorage || BatString.starts_with x.vname "__builtin"))
+         (fun x -> not (isExtern x.vstorage || String.starts_with x.vname ~prefix:"__builtin"))
          (neigbourFunction fd.svar)
       )
     ;

src/build-info/dune

@@ -8,7 +8,6 @@
 (library
   (name goblint_build_info)
   (public_name goblint.build-info)
-  (libraries batteries.unthreaded)
   (virtual_modules dune_build_info))
 
 (rule

src/build-info/goblint_build_info.ml

@@ -18,7 +18,7 @@ let release_commit = "%%VCS_COMMIT_ID%%"
 (** Goblint version. *)
 let version =
   let commit = ConfigVersion.version in
-  if BatString.starts_with release_version "%" then
+  if String.starts_with release_version ~prefix:"%" then
     commit
   else (
     let commit =

src/cdomain/value/domains/invariantCil.ml

@@ -88,7 +88,7 @@ class exp_contains_anon_type_visitor = object
   inherit nopCilVisitor
   method! vtype (t: typ) =
     match t with
-    | TComp ({cname; _}, _) when BatString.starts_with_stdlib ~prefix:"__anon" cname ->
+    | TComp ({cname; _}, _) when String.starts_with ~prefix:"__anon" cname ->
       raise Stdlib.Exit
     | _ ->
       DoChildren
@@ -102,7 +102,7 @@ let exp_contains_anon_type =
 
 
 (* TODO: synchronize magic constant with BaseDomain *)
-let var_is_heap {vname; _} = BatString.starts_with vname "(alloc@"
+let var_is_heap {vname; _} = String.starts_with vname ~prefix:"(alloc@"
 
 let reset_lazy () =
   ResettableLazy.reset exclude_vars_regexp

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -6,7 +6,6 @@
     Matrices are modeled as proposed by Karr: Each variable is assigned to a column and each row represents a linear affine relationship that must hold at the corresponding program point.
     The apron environment is hereby used to organize the order of columns and variables. *)
 
-open Batteries
 open GoblintCil
 open Pretty
 module M = Messages
@@ -193,7 +192,7 @@ struct
       in
       let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars)
                 ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in
-      if String.starts_with res "+" then
+      if String.starts_with res ~prefix:"+" then
         Str.string_after res 1
       else
         res
@@ -369,7 +368,7 @@ struct
   let remove_rels_with_var x var env inplace = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) inplace
 
   let forget_vars t vars =
-    if is_bot t || is_top_env t || List.is_empty vars then
+    if is_bot t || is_top_env t || vars = [] then
       t
     else
       let m = Option.get t.d in

src/common/util/cilfacade.ml

@@ -734,7 +734,7 @@ let add_function_declarations (file: Cil.file): unit =
   let functions, non_functions = List.partition (fun g -> match g with GFun _ -> true | _ -> false) globals in
   let upto_last_type, non_types = GobList.until_last_with (fun g -> match g with GType _ -> true | _ -> false) non_functions in
   let declaration_from_GFun f = match f with
-    | GFun (f, _) when BatString.starts_with_stdlib ~prefix:"__builtin" f.svar.vname ->
+    | GFun (f, _) when String.starts_with ~prefix:"__builtin" f.svar.vname ->
       (* Builtin functions should not occur in asserts generated, so there is no need to add declarations for them.*)
       None
     | GFun (f, _) ->

src/domains/access.ml

@@ -1,6 +1,5 @@
 (** Memory accesses and their manipulation. *)
 
-open Batteries
 open GoblintCil
 open Pretty
 open GobConfig
@@ -12,7 +11,7 @@ module M = Messages
 
 let is_ignorable_comp_name = function
   | "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag" | "_IO_FILE" -> true
-  | cname when String.starts_with_stdlib ~prefix:"__anon" cname ->
+  | cname when String.starts_with ~prefix:"__anon" cname ->
     begin match Cilfacade.split_anoncomp_name cname with
       | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
       | (false, Some ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
@@ -385,7 +384,7 @@ and distribute_access_exp f = function
 
 and distribute_access_type f = function
   | TArray (et, len, _) ->
-    Option.may (distribute_access_exp f) len;
+    Option.iter (distribute_access_exp f) len;
     distribute_access_type f et
 
   | TVoid _
@@ -434,7 +433,7 @@ struct
   include SetDomain.Make (A)
 
   let max_conf accs =
-    accs |> elements |> List.map (fun {A.conf; _} -> conf) |> (List.max ~cmp:Int.compare)
+    accs |> elements |> List.map (fun {A.conf; _} -> conf) |> (BatList.max ~cmp:Int.compare)
 end
 
 
@@ -583,7 +582,7 @@ let incr_summary ~safe ~vulnerable ~unsafe grouped_accs =
     |> List.filter_map race_conf
     |> (function
         | [] -> None
-        | confs -> Some (List.max confs)
+        | confs -> Some (BatList.max confs)
       )
   in
   match safety with

src/incremental/compareAST.ml

@@ -73,7 +73,7 @@ let forward_list_equal ?(propF = (&&>>)) f l1 l2 ~(rename_mapping: rename_mappin
 let compare_name (a: string) (b: string) =
   let anon_struct = "__anonstruct_" in
   let anon_union = "__anonunion_" in
-  if a = b then true else BatString.(starts_with a anon_struct && starts_with b anon_struct || starts_with a anon_union && starts_with b anon_union)
+  if a = b then true else String.(starts_with a ~prefix:anon_struct && starts_with b ~prefix:anon_struct || starts_with a ~prefix:anon_union && starts_with b ~prefix:anon_union)
 
 let rec eq_constant ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) (a: constant) (b: constant) : bool * rename_mapping =
   match a, b with

src/incremental/makefileUtil.ml

@@ -39,7 +39,7 @@ let find_file_by_suffix (dir: Fpath.t) (file_name_suffix: string) =
     | (h::t) -> let f = Fpath.to_string h in
       if Sys.file_exists f && Sys.is_directory f
       then (Queue.add h dirs; search dir t)
-      else if Batteries.String.ends_with (Fpath.filename h) file_name_suffix then h else search dir t
+      else if String.ends_with (Fpath.filename h) ~suffix:file_name_suffix then h else search dir t
     | [] ->
       if Queue.is_empty dirs then failwith ("find_file_by_suffix found no files with suffix "^file_name_suffix^" in "^ Fpath.to_string dir)
       else let d = Queue.take dirs in search d (list_files d)

src/witness/svcomp.ml

@@ -1,7 +1,6 @@
 (** SV-COMP tasks and results. *)
 
 open GoblintCil
-open Batteries
 
 module Specification = SvcompSpec
 
@@ -27,9 +26,9 @@ let is_error_function f =
 (* TODO: unused, but should be used? *)
 let is_special_function f =
   let loc = f.vdecl in
-  let is_svcomp = String.ends_with loc.file "sv-comp.c" in (* only includes/sv-comp.c functions, not __VERIFIER_assert in benchmark *)
+  let is_svcomp = String.ends_with loc.file ~suffix:"sv-comp.c" in (* only includes/sv-comp.c functions, not __VERIFIER_assert in benchmark *)
   let is_verifier = match f.vname with
-    | fname when String.starts_with fname "__VERIFIER" -> true
+    | fname when String.starts_with fname ~prefix:"__VERIFIER" -> true
     | fname -> is_error_function f
   in
   is_svcomp && is_verifier