[Eva] Partition: creates the split_monitor once when building the split action.

And not at each application of the split action.

src/plugins/value/engine/partition.ml

@@ -174,7 +174,7 @@ type action =
   | Branch of branch * int
   | Ration of rationing
   | Restrict of Cil_types.exp * Integer.t list
-  | Split of Cil_types.exp * split_kind * int
+  | Split of Cil_types.exp * split_kind * split_monitor
   | Merge of Cil_types.exp * split_kind
   | Update_dynamic_splits
 
@@ -363,8 +363,7 @@ struct
     with Operation_failed ->
       [(key,state)]
 
-  let split ~limit (kind : split_kind) (exp : Cil_types.exp) (p : t) =
-    let monitor = new_monitor limit in
+  let split ~monitor (kind : split_kind) (exp : Cil_types.exp) (p : t) =
     let add_split acc (key,state) =
       split_state ~monitor kind exp key state @ acc
     in
@@ -389,8 +388,8 @@ struct
     List.map (fun (k,x) -> f k x, x) p
 
   let transfer_keys p = function
-    | Split (expr, kind, limit) ->
-      split ~limit kind expr p
+    | Split (expr, kind, monitor) ->
+      split ~monitor kind expr p
 
     | Update_dynamic_splits ->
       update_dynamic_splits p

src/plugins/value/engine/partition.mli

@@ -90,6 +90,12 @@ type unroll_limit =
       states are then split or merged accordingly. *)
 type split_kind = Static | Dynamic
 
+(** Split monitor: prevents splits from generating too many states. *)
+type split_monitor
+
+(** Creates a new monitor that allows to split up to [split_limit] states. *)
+val new_monitor: split_limit:int -> split_monitor
+
 (** These actions redefine the partitioning by updating keys or spliting states.
     They are applied to all the pair (key, state) in a flow. *)
 type action =
@@ -127,12 +133,14 @@ type action =
       - all other states are joined together.
       Previous rationing is erased and replaced by this new stamping.
       Implementation of the option -eva-split-return. *)
-  | Split of Cil_types.exp * split_kind * int
-  (** [Split (exp, kind, max)] tries to separate states such as the [exp]
+  | Split of Cil_types.exp * split_kind * split_monitor
+  (** [Split (exp, kind, monitor)] tries to separate states such as the [exp]
       evaluates to a singleton value in each state in the flow. If necessary and
       possible, splits states into multiple states. States in which the [exp]
       evaluates to different values will be kept separate. Gives up the split
-      if [exp] evaluates to more than [max] values. *)
+      if [exp] evaluates to more than [limit] values, [limit] being the split
+      limit of the [monitor]. A same monitor can be used for successive splits
+      on different flows. *)
   | Merge of Cil_types.exp * split_kind
   (** Forgets the split of an expression: states that were kept separate only
       by the split of this expression will be joined together. *)

src/plugins/value/engine/partitioning_parameters.ml

@@ -109,7 +109,8 @@ struct
     let add name l =
       try
         let vi = Globals.Vars.find_from_astinfo name VGlobal in
-        Partition.Split (Cil.evar vi, Partition.Dynamic, split_limit) :: l
+        let monitor = Partition.new_monitor ~split_limit in
+        Partition.Split (Cil.evar vi, Partition.Dynamic, monitor) :: l
       with Not_found ->
         warn ~current:false "cannot find the global variable %s for value \
                              partitioning" name;
@@ -121,9 +122,10 @@ struct
     let kind = Partition.Static in
     let map_annot acc t =
       try
+        let monitor = Partition.new_monitor ~split_limit in
         let action =
           match t with
-          | FlowSplit t -> Partition.Split (term_to_exp t, kind, split_limit)
+          | FlowSplit t -> Partition.Split (term_to_exp t, kind, monitor)
           | FlowMerge t -> Partition.Merge (term_to_exp t, kind)
         in
         action :: acc