diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 7f7451c7ae1a27ba1a73ccba3fe01ef2e5607efb..3c7cfb73c2ebce2e30cda2f42da7574861076aec 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -771,6 +771,15 @@ let fold f =
by_emitter
acc)
+let to_seq () =
+ State.to_seq () |>
+ Seq.flat_map (fun (_,emitter) -> Usable_emitter.Hashtbl.to_seq emitter) |>
+ Seq.flat_map
+ (fun (e,h) ->
+ D.Hashtbl.to_seq h |>
+ Seq.map (fun (alarm, (annot, kf, stmt, rank)) ->
+ Usable_emitter.get e, kf, stmt, rank, alarm, annot))
+
let find annot =
try Some (Alarm_of_annot.find annot)
with Not_found -> None
diff --git a/src/kernel_services/ast_data/alarms.mli b/src/kernel_services/ast_data/alarms.mli
index adfe341aaf4c5b959955bf27e3c78bbf0c80f308..ffaf67de138d8e4f7eeecfd2d8c943303613460f 100644
--- a/src/kernel_services/ast_data/alarms.mli
+++ b/src/kernel_services/ast_data/alarms.mli
@@ -105,6 +105,13 @@ val fold:
point.
@since Fluorine-20130401 *)
+val to_seq:
+ unit ->
+ (Emitter.t * kernel_function * stmt * int * alarm * code_annotation) Seq.t
+(** Returns the sequence of all alarms and the associated annotations at some
+ program point
+ @since Frama-C+dev *)
+
val find: code_annotation -> alarm option
(** @return the alarm corresponding to the given assertion, if any.
@since Fluorine-20130401 *)
diff --git a/src/kernel_services/plugin_entry_points/emitter.ml b/src/kernel_services/plugin_entry_points/emitter.ml
index 0349a71692e9d42ea2aefbe5fbb1453c10155f4a..bdcd37227adb7ce862c9560cedc8a83c1472e4c1 100644
--- a/src/kernel_services/plugin_entry_points/emitter.ml
+++ b/src/kernel_services/plugin_entry_points/emitter.ml
@@ -636,6 +636,7 @@ struct
let mem key = H.mem !state key
let iter f = H.iter f !state
let fold f acc = H.fold f !state acc
+ let to_seq () = H.to_seq !state
let iter_sorted ~cmp f = H.iter_sorted ~cmp f !state
let fold_sorted ~cmp f acc = H.fold_sorted ~cmp f !state acc
let remove key =
diff --git a/src/kernel_services/plugin_entry_points/emitter.mli b/src/kernel_services/plugin_entry_points/emitter.mli
index 96e4ae157d547da175a300d28f0a2def5ef33e85..402a17ba6fddac2671851a59bbfbf8af0df88fbd 100644
--- a/src/kernel_services/plugin_entry_points/emitter.mli
+++ b/src/kernel_services/plugin_entry_points/emitter.mli
@@ -136,6 +136,7 @@ sig
val mem: H.key -> bool
val iter: (H.key -> internal_tbl -> unit) -> unit
val fold: (H.key -> internal_tbl -> 'a -> 'a) -> 'a -> 'a
+ val to_seq: unit -> (H.key * internal_tbl) Seq.t
val iter_sorted:
cmp: (H.key -> H.key -> int) -> (H.key -> internal_tbl -> unit) -> unit
val fold_sorted:
diff --git a/src/libraries/stdlib/transitioning.ml b/src/libraries/stdlib/transitioning.ml
index 0ca1ea3afa5463c2237ea4363182b2dc7a2f4bcf..f11d88cb8a4a5ae5b86380cc0a7b66bb6f418b58 100644
--- a/src/libraries/stdlib/transitioning.ml
+++ b/src/libraries/stdlib/transitioning.ml
@@ -45,3 +45,15 @@ module List = struct
let n = f x1 x2 in
if n = 0 then compare f q1 q2 else n
end
+
+
+module Seq = struct
+ open Stdlib.Seq
+
+ let mapi f seq =
+ let i = ref 0 in
+ map (fun x -> let y = f !i x in incr i; y) seq
+
+ let unzip seq =
+ map fst seq, map snd seq
+end
diff --git a/src/libraries/stdlib/transitioning.mli b/src/libraries/stdlib/transitioning.mli
index cb378f0cd9c0dac9102f58857be04f54eae18a2e..be40531442b3ef2af3bbd28f313dd78beea4a80e 100644
--- a/src/libraries/stdlib/transitioning.mli
+++ b/src/libraries/stdlib/transitioning.mli
@@ -42,3 +42,11 @@ module List: sig
(** since 4.12.0 *)
val compare: ('a -> 'a -> int) -> 'a list -> 'a list -> int
end
+
+module Seq: sig
+ (** since 4.14.0 *)
+ val mapi: (int -> 'a -> 'b) -> 'a Seq.t -> 'b Seq.t
+
+ (** since 4.14.0 *)
+ val unzip : ('a * 'b) Seq.t -> 'a Seq.t * 'b Seq.t
+end
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 7378f6b6b85eaaf91cb59bc239328a692d3956a3..6845c703cfde80127a09f25068071efcca492b2d 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -161,31 +161,27 @@ let opt_physical_location_of_loc loc =
else [ Location.of_loc loc ]
(* Cil_types *)
let gen_results remarks =
- let treat_alarm _e kf s ~rank:_ alarm annot (i, rules, content) =
- if not (Mdr_params.PrintLibc.get ()) && kf_is_in_libc kf then
- (* skip alarm in libc *)
- (i, rules, content)
- else
- let prop = Property.ip_of_code_annot_single kf s annot in
- let ruleId = Alarms.get_name alarm in
- let rules =
- Datatype.String.Map.add ruleId (Alarms.get_description alarm) rules
- in
- let label = "Alarm-" ^ string_of_int i in
- let kind = kind_of_status (Property_status.Feedback.get prop) in
- let level = level_of_status (Property_status.Feedback.get prop) in
- let remark = get_remark remarks label in
- let message = make_message alarm annot remark in
- let locations = opt_physical_location_of_loc (Cil_datatype.Stmt.loc s) in
- let res =
- Sarif_result.create ~kind ~level ~ruleId ~message ~locations ()
- in
- (i+1, rules, res :: content)
+ let keep_alarm (_,kf,_,_,_,_) =
+ (* skip alarm in libc *)
+ Mdr_params.PrintLibc.get () || not (kf_is_in_libc kf)
+ in
+ let treat_alarm i (_e,kf,s,_rank,alarm,annot) =
+ let prop = Property.ip_of_code_annot_single kf s annot in
+ let ruleId = Alarms.get_name alarm in
+ let label = "Alarm-" ^ string_of_int i in
+ let kind = kind_of_status (Property_status.Feedback.get prop) in
+ let level = level_of_status (Property_status.Feedback.get prop) in
+ let remark = get_remark remarks label in
+ let message = make_message alarm annot remark in
+ let locations = opt_physical_location_of_loc (Cil_datatype.Stmt.loc s) in
+ let res = Sarif_result.create ~kind ~level ~ruleId ~message ~locations () in
+ (ruleId, Alarms.get_description alarm), res
in
- let _, rules, content =
- Alarms.fold treat_alarm (0, Datatype.String.Map.empty,[])
+ let rules, content =
+ Alarms.to_seq () |> Seq.filter keep_alarm |>
+ Transitioning.Seq.mapi treat_alarm |> Transitioning.Seq.unzip
in
- rules, List.rev content
+ Datatype.String.Map.of_seq rules, List.of_seq content
let is_alarm = function
| Property.(IPCodeAnnot { ica_ca }) -> Option.is_some (Alarms.find ica_ca)