diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml index 17ae93256275156c24a8165202a06f6c7b5418f2..8300fb92d130d1f72e0304d3fbe8d6267a33a098 100644 --- a/src/plugins/value/engine/iterator.ml +++ b/src/plugins/value/engine/iterator.ml @@ -88,9 +88,10 @@ module Make_Dataflow (* Ideally, the slevel parameter should not be used anymore in this file but it is still required for logic interpretation *) - let slevel = + let slevel, history_size = let module P = Partitioning_parameters.Make (AnalysisParam) in - P.slevel + P.slevel, + P.history_size (* --- Abstract values storage --- *) @@ -281,7 +282,8 @@ module Make_Dataflow (* Propagate info that the current call cannot be cached either *) cacheable := Eval.NoCacheCallers; (* Recombine callee partitioning keys with caller key *) - List.map (fun (k,s) -> Partition.Key.recombine key k, s) result + let recombine = Partition.Key.recombine ~history_size in + List.map (fun (k,s) -> recombine key k, s) result let transfer_instr (stmt : stmt) (instr : instr) : transfer_function = match instr with diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml index 6919f7e7e73302baadc9095960ff7393f8b29f1c..49a4ef331b83d4b862831806ca665ff6f46e3189 100644 --- a/src/plugins/value/partitioning/partition.ml +++ b/src/plugins/value/partitioning/partition.ml @@ -243,15 +243,15 @@ struct let exceed_rationing key = key.ration_stamp = None - let recombine k1 k2 = + let recombine ~history_size k1 k2 = let merge_split _ v1 v2 = match v1, v2 with | None, None -> None | Some v, None | None, Some v -> Some v | Some _v1, Some v2 -> Some v2 (* Keep the newest split value *) in { - ration_stamp = k2.ration_stamp; - branches = k2.branches @ k1.branches; + ration_stamp = None; + branches = Extlib.list_first_n history_size (k2.branches @ k1.branches); loops = k1.loops; splits = SplitMap.merge merge_split k1.splits k2.splits; dynamic_splits = diff --git a/src/plugins/value/partitioning/partition.mli b/src/plugins/value/partitioning/partition.mli index 662995e4053fdaa839f10c9a0f6d6da96174d967..d894e23fc842b42ee9882356bc48aee8607e71f5 100644 --- a/src/plugins/value/partitioning/partition.mli +++ b/src/plugins/value/partitioning/partition.mli @@ -45,7 +45,8 @@ module Key : sig include Datatype.S_with_collections with type t = key val zero : t (** Initial key: no partitioning. *) val exceed_rationing: t -> bool - val recombine : t -> t -> t (** Recombinaison of keys after a call *) + val recombine : history_size:int -> + t -> t -> t (** Recombinaison of keys after a call *) end (** Collection of states, each identified by a unique key. *) diff --git a/tests/value/oracle/partitioning-interproc.0.res.oracle b/tests/value/oracle/partitioning-interproc.0.res.oracle index 32cae5f42582c2fcf9a62d0539a76062b20e8a85..4481fdb71c75b560b40d5f611f615da44aa446a3 100644 --- a/tests/value/oracle/partitioning-interproc.0.res.oracle +++ b/tests/value/oracle/partitioning-interproc.0.res.oracle @@ -23,7 +23,6 @@ [eva] Recording results for cassign [eva] Done for function cassign [eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1} -[eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1} [eva] Recording results for cassign_test [eva] done for function cassign_test [eva] ====== VALUES COMPUTED ======