diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index fe0c8bbf67e4f83d23c396f930fa6bdb52bbcf31..a33ba44e4a4086fda409023222c21278420b60db 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -589,6 +589,9 @@ let fold_global f =
h
acc)
+let iter_behaviors f kf =
+ List.iter f (behaviors kf)
+
let iter_spec_gen get iter f kf =
try
let tbl = Funspecs.find kf in
@@ -604,7 +607,7 @@ let iter_spec_gen get iter f kf =
with Not_found ->
()
-let iter_behaviors f =
+let iter_behaviors_by_emitter f =
iter_spec_gen
(fun s -> s.spec_behavior)
(fun f l -> List.iter (fun b -> f { b with b_name = b.b_name}) l)
@@ -657,6 +660,9 @@ let iter_allocates f =
let iter_extended f = iter_bhv_gen (fun b -> b.b_extended) List.iter f
+let fold_behaviors f kf acc =
+ List.fold_left (Fun.flip f) acc (behaviors kf)
+
let fold_spec_gen get fold f kf acc =
try
let tbl = Funspecs.find kf in
@@ -672,7 +678,7 @@ let fold_spec_gen get fold f kf acc =
with Not_found ->
acc
-let fold_behaviors f =
+let fold_behaviors_by_emitter f =
fold_spec_gen
(fun s -> s.spec_behavior)
(fun f l acc ->
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index d503ea5bd03b8d7b9ec1d92fb90cc8e8114d24fe..17b568e01cc5bd05ed5fa572b5532a6d8deb2410 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -225,13 +225,27 @@ val fold_extended:
kernel_function -> string -> 'a -> 'a
val iter_behaviors:
- (Emitter.t -> funbehavior -> unit) -> kernel_function -> unit
+ (funbehavior -> unit) -> kernel_function -> unit
(** Iter on the behaviors of the given kernel function.
- @since Fluorine-20130401 *)
+ @since Fluorine-20130401
+ @before Frama-C+dev previous version was behaving as
+ {!iter_behaviors_by_emitter} *)
val fold_behaviors:
+ (funbehavior -> 'a -> 'a) -> kernel_function -> 'a -> 'a
+(** Fold on the behaviors of the given kernel function.
+ @before Frama-C+dev previous version was behaving as
+ {!fold_behaviors_by_emitter} *)
+
+val iter_behaviors_by_emitter:
+ (Emitter.t -> funbehavior -> unit) -> kernel_function -> unit
+(** Iter on the behaviors, for each emitter, of the given kernel function.
+ @since Frama-C+dev *)
+
+val fold_behaviors_by_emitter:
(Emitter.t -> funbehavior -> 'a -> 'a) -> kernel_function -> 'a -> 'a
-(** Fold on the behaviors of the given kernel function. *)
+(** Fold on the behaviors, for each emitter, of the given kernel function.
+ @since Frama-C+dev *)
val iter_complete:
(Emitter.t -> string list -> unit) -> kernel_function -> unit
diff --git a/src/kernel_services/visitors/visitor.ml b/src/kernel_services/visitors/visitor.ml
index 2dc1b32fcad19835139430f115705a1b9654f3f2..32487e3fa067cba9526f03cb0f299b560b452381 100644
--- a/src/kernel_services/visitors/visitor.ml
+++ b/src/kernel_services/visitors/visitor.ml
@@ -390,7 +390,7 @@ class internal_generic_frama_c_visitor fundec queue current_kf behavior: frama_c
let kf = Option.get self#current_kf in
let new_kf = Visitor_behavior.Get.kernel_function self#behavior kf in
let old_behaviors =
- Annotations.fold_behaviors (fun e b acc -> (e,b)::acc) kf []
+ Annotations.fold_behaviors_by_emitter (fun e b acc -> (e,b)::acc) kf []
in
let old_complete =
Annotations.fold_complete (fun e c acc -> (e,c)::acc) kf []
diff --git a/src/plugins/e-acsl/examples/demo/script.ml b/src/plugins/e-acsl/examples/demo/script.ml
index bca0d3708ad9c754898d14f3b2c44edfc8bc5ef7..bcf4625f4ff0e5c925c42998ab78702abc6beb56 100644
--- a/src/plugins/e-acsl/examples/demo/script.ml
+++ b/src/plugins/e-acsl/examples/demo/script.ml
@@ -63,7 +63,7 @@ let is_predicate p line = (fst (p.ip_loc)).Lexing.pos_lnum = line
let search_funspec_part iter convert kf =
try
Annotations.iter_behaviors
- (fun _ bhv -> iter (fun _ a -> convert bhv a) kf bhv.b_name)
+ (fun bhv -> iter (fun _ a -> convert bhv a) kf bhv.b_name)
kf;
assert false
with Found(ppt, line) ->
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index 11cf5f2420a856a6f737b59f10d5a41aed664029..ddc26d216b4f54386a5f386dffa1a6f1bb6df97f 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -460,7 +460,7 @@ module rec Transfer
let state =
if (is_first || is_last) && Functions.RTL.is_generated_kf kf then
Annotations.fold_behaviors
- (fun _ bhv s ->
+ (fun bhv s ->
let handle_annot test f s =
if test then
f
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
index ba0d33bb5641c02b1f7d7b44d8b626528274a73e..12286c8e69bc9c50731fb4341a7f2fce432f1dd7 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -253,7 +253,7 @@ let dup_global loc spec sound_verdict_vi kf vi new_vi =
with neither contract nor body *)
if Kernel_function.is_definition kf then begin
let old_bhvs =
- Annotations.fold_behaviors (fun e b acc -> (e, b) :: acc) kf []
+ Annotations.fold_behaviors_by_emitter (fun e b acc -> (e, b) :: acc) kf []
in
List.iter
(fun (e, b) -> Annotations.remove_behavior ~force:true e kf b)
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index 48b2f08ee23fae975c0d7e64b8e6ccc9d066a0fe..3310e454ec3de0298e160b8b621c3671a410aaf7 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -145,7 +145,7 @@ let compute_postconditions_statuses kf =
List.iter validate_property
(Property.ip_post_cond_of_behavior kf ~active:[] Kglobal bhv)
in
- Annotations.iter_behaviors (fun _ -> posts) kf
+ Annotations.iter_behaviors posts kf
let compute_comp_disj_statuses kf =
let open Property in
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index 0ead13ca412c7d997bfc523f35b10d3ea0d19363..a351c3b1f807b3c7cdd23358da369a9e58e02dcb 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -230,7 +230,7 @@ let treat_behavior local_stats ki b =
let add_function_contract_stats kf =
let local_stats = get_kf_stats kf in
- let treat_behavior _ b = treat_behavior local_stats Kglobal b in
+ let treat_behavior b = treat_behavior local_stats Kglobal b in
Annotations.iter_behaviors treat_behavior kf
let add_code_annot_stats stmt _ ca =
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index fba8a49e215abae7019981c079bb1fca1763026a..15836739fa4b32e075c28ef6cc6b50abcff3fe77 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -212,7 +212,7 @@ let obfuscate_behaviors () =
Globals.Functions.iter
(fun kf ->
let h = Datatype.String.Hashtbl.create 7 in
- Annotations.iter_behaviors
+ Annotations.iter_behaviors_by_emitter
(fun emitter b ->
if Emitter.equal emitter Emitter.end_user
&& not (Cil.is_default_behavior b)
diff --git a/src/plugins/wp/wpTarget.ml b/src/plugins/wp/wpTarget.ml
index cc0d7384a984cc41835a6cb994de8ed578a3365c..19c3fc2c81bdfeced8458317a8b474a3adffbe5e 100644
--- a/src/plugins/wp/wpTarget.ml
+++ b/src/plugins/wp/wpTarget.ml
@@ -149,7 +149,7 @@ let check_properties behaviors props kf =
in
List.iter check_stmt stmts
in
- let check_funbhv _ bv = check_bhv kf Kglobal bv in
+ let check_funbhv bv = check_bhv kf Kglobal bv in
Annotations.iter_behaviors check_funbhv kf ;
check_code ()
diff --git a/tests/libc/check_libc_naming_conventions.ml b/tests/libc/check_libc_naming_conventions.ml
index bb8b128d2960a1baded2d1a0b9fd84d5db0b14ce..29354de5799f2a91050f5f8b36255f1b4dd1b6d6 100644
--- a/tests/libc/check_libc_naming_conventions.ml
+++ b/tests/libc/check_libc_naming_conventions.ml
@@ -56,7 +56,7 @@ let () =
| Declaration (_, vi, _, _) -> vi.vattr
in
if Cil.is_in_libc fun_attrs then begin
- Annotations.iter_behaviors (fun _emitter bhv ->
+ Annotations.iter_behaviors (fun bhv ->
List.iter (fun ip ->
let pred = Logic_const.pred_of_id_pred ip in
warn_if_unnamed "requires" pred;