Skip to content

Commit d002355

Browse files
committed
moved the CheckMap related code to the top level of the checks.ml
1 parent 9b1aaa8 commit d002355

File tree

1 file changed

+61
-60
lines changed

1 file changed

+61
-60
lines changed

src/common/util/checks.ml

Lines changed: 61 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -99,70 +99,71 @@ module Check = struct
9999
Kind.pp check.kind
100100
check.messages
101101
(Format.pp_print_option CilType.Location.pp) check.range
102-
module CheckMap = Hashtbl.Make (struct
103-
type nonrec t = t
104-
let equal = equal
105-
let hash = hash
106-
end)
107-
108-
109-
module CategoryLocationMap = Hashtbl.Make (struct
110-
type t = Category.t * CilType.Location.t [@@deriving hash, eq]
111-
end)
112-
113-
114-
let checks_list : (bool ref * unit CheckMap.t) CategoryLocationMap.t = CategoryLocationMap.create 113
115-
116-
let add_check check =
117-
match check.range with
118-
| Some range -> (
119-
(* Mark all ranges as synthetic for hash purposes *)
120-
let range = { range with synthetic = true } in
121-
let check = { check with range = Some range } in
122-
let check_key = (check.title, range) in
123-
match CategoryLocationMap.find_opt checks_list check_key with
124-
| Some (safe, existing_checks) ->
125-
if !safe && Kind.is_safe check.kind then
126-
CheckMap.replace existing_checks check ()
127-
else if not @@ Kind.is_safe check.kind then (
128-
if !safe then CheckMap.clear existing_checks;
129-
safe := false;
130-
CheckMap.replace existing_checks check ()
131-
)
132-
| None ->
133-
let table = CheckMap.create 10 in
134-
CheckMap.replace table check ();
135-
CategoryLocationMap.replace checks_list check_key (ref (Kind.is_safe check.kind), table))
136-
| None ->
137-
()
138-
139-
let check kind title fmt =
140-
if !AnalysisState.should_warn then (
141-
let finish doc =
142-
let loc = Option.map UpdateCil0.getLoc !Node0.current_node in
143-
let messages = GobPretty.show doc in
144-
let check = make ~kind ~title ?range:loc ~messages () in
145-
add_check check in
146-
GoblintCil.Pretty.gprintf finish fmt)
147-
else
148-
GobPretty.igprintf () fmt
149-
150-
151-
let export () =
152-
`List (
153-
List.map to_yojson @@ CategoryLocationMap.fold (
154-
fun _ (checks: (bool ref * unit CheckMap.t)) acc ->
155-
List.rev_append (CheckMap.to_seq_keys @@ snd checks |> List.of_seq) acc
156-
) checks_list []
157-
)
158102
end
159103

160-
let error category = Check.check Kind.Error category
161-
162-
let warn category = Check.check Kind.Warning category
104+
module CheckMap = Hashtbl.Make (struct
105+
type t = Check.t
106+
let equal = Check.equal
107+
let hash = Check.hash
108+
end)
109+
110+
111+
module CategoryLocationMap = Hashtbl.Make (struct
112+
type t = Category.t * CilType.Location.t [@@deriving hash, eq]
113+
end)
114+
115+
116+
let checks_list : (bool ref * unit CheckMap.t) CategoryLocationMap.t = CategoryLocationMap.create 113
117+
118+
let add_check check =
119+
match check.Check.range with
120+
| Some range -> (
121+
(* Mark all ranges as synthetic for hash purposes *)
122+
let range = { range with synthetic = true } in
123+
let check = { check with range = Some range } in
124+
let check_key = (check.title, range) in
125+
match CategoryLocationMap.find_opt checks_list check_key with
126+
| Some (safe, existing_checks) ->
127+
if !safe && Kind.is_safe check.kind then
128+
CheckMap.replace existing_checks check ()
129+
else if not @@ Kind.is_safe check.kind then (
130+
if !safe then CheckMap.clear existing_checks;
131+
safe := false;
132+
CheckMap.replace existing_checks check ()
133+
)
134+
| None ->
135+
let table = CheckMap.create 10 in
136+
CheckMap.replace table check ();
137+
CategoryLocationMap.replace checks_list check_key (ref (Kind.is_safe check.kind), table))
138+
| None ->
139+
()
140+
141+
let check kind title fmt =
142+
if !AnalysisState.should_warn then (
143+
let finish doc =
144+
let loc = Option.map UpdateCil0.getLoc !Node0.current_node in
145+
let messages = GobPretty.show doc in
146+
let check = Check.make ~kind ~title ?range:loc ~messages () in
147+
add_check check in
148+
GoblintCil.Pretty.gprintf finish fmt)
149+
else
150+
GobPretty.igprintf () fmt
151+
152+
153+
let export () =
154+
`List (
155+
List.map Check.to_yojson @@ CategoryLocationMap.fold (
156+
fun _ (checks: (bool ref * unit CheckMap.t)) acc ->
157+
List.rev_append (CheckMap.to_seq_keys @@ snd checks |> List.of_seq) acc
158+
) checks_list []
159+
)
160+
161+
let error category = check Kind.Error category
162+
163+
let warn category = check Kind.Warning category
163164

164165
let safe ?(message = "") category =
165166
match !Node0.current_node with
166167
| Some (Statement _) ->
167-
Check.check Kind.Safe category "%s" message
168+
check Kind.Safe category "%s" message
168169
| _ -> ()

0 commit comments

Comments
 (0)