[Interpreted_automata] dataflow analysis: implements an ordered iteration over results

src/kernel_services/analysis/interpreted_automata.ml

@@ -1215,6 +1215,7 @@ sig
     val after : result -> Cil_types.stmt -> state option
     val iter_vertex : (vertex -> state -> unit) -> result -> unit
     val iter_stmt : (Cil_types.stmt -> state -> unit) -> result -> unit
+    val iter_stmt_asc : (Cil_types.stmt -> state -> unit) -> result -> unit
     val to_dot_output : (Format.formatter -> state -> unit) ->
       result -> out_channel -> unit
     val to_dot_file : (Format.formatter -> state -> unit) ->
@@ -1324,6 +1325,19 @@ struct
       in
       States.iter f' states
 
+    let iter_stmt_asc f (_automaton,_wto,states) =
+      let filter (v,s) =
+        match v.vertex_start_of with
+        | None -> None
+        | Some stmt -> Some (stmt,s)
+      in
+      let cmp (stmt1,_) (stmt2,_) =
+        stmt1.sid - stmt2.sid
+      in
+      States.to_seq states |> Seq.filter_map filter |>
+      List.of_seq |> List.fast_sort cmp |>
+      List.iter (fun (stmt,s) -> f stmt s)
+
     let to_dot_output pp_value (automaton,wto,states) out =
       let pp_vertex fmt v =
         match States.find_opt states v with

src/kernel_services/analysis/interpreted_automata.mli

@@ -347,6 +347,10 @@ sig
         returned None) *)
     val iter_stmt : (Cil_types.stmt -> state -> unit) -> result -> unit
 
+    (** Same as [iter_stmt] but guarantee that the iteration will always
+        be in the same increasing order of statements sid *)
+    val iter_stmt_asc : (Cil_types.stmt -> state -> unit) -> result -> unit
+
     (** Output result to the given channel. Must be supplied with a pretty
         printer for abstract values *)
     val to_dot_output : (Format.formatter -> state -> unit) ->