Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use String.starts_with and ends_with from Stdlib #1523

Merged
merged 1 commit into from
Sep 9, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions src/analyses/mutexEventsAnalysis.ml
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@
module M = Messages
module Addr = ValueDomain.Addr
module LF = LibraryFunctions
open Batteries
open GoblintCil
open Analyses
open GobConfig
Expand Down Expand Up @@ -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 =
Expand Down
2 changes: 1 addition & 1 deletion src/autoTune.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
)
;
Expand Down
1 change: 0 additions & 1 deletion src/build-info/dune
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
(library
(name goblint_build_info)
(public_name goblint.build-info)
(libraries batteries.unthreaded)
(virtual_modules dune_build_info))

(rule
Expand Down
2 changes: 1 addition & 1 deletion src/build-info/goblint_build_info.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
4 changes: 2 additions & 2 deletions src/cdomain/value/domains/invariantCil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
5 changes: 2 additions & 3 deletions src/cdomains/apron/affineEqualityDomain.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -370,7 +369,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
Expand Down
2 changes: 1 addition & 1 deletion src/common/util/cilfacade.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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, _) ->
Expand Down
9 changes: 4 additions & 5 deletions src/domains/access.ml
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
(** Memory accesses and their manipulation. *)

open Batteries
open GoblintCil
open Pretty
open GobConfig
Expand All @@ -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 *)
Expand Down Expand Up @@ -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 _
Expand Down Expand Up @@ -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


Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/incremental/compareAST.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/incremental/makefileUtil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
5 changes: 2 additions & 3 deletions src/witness/svcomp.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
(** SV-COMP tasks and results. *)

open GoblintCil
open Batteries

module Specification = SvcompSpec

Expand All @@ -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
Expand Down
Loading