diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml index da3c224a4f0b3918041429c36373933a66193cbf..caa9aa30249edf29ed6e2777e92fa9fa348227c0 100644 --- a/src/plugins/e-acsl/pre_analysis.ml +++ b/src/plugins/e-acsl/pre_analysis.ml @@ -220,8 +220,7 @@ module rec Transfer ignore (Visitor.visitFramacIdPredicate (register state_ref) pred); !state_ref in - let register_code_annot annot state = - let a = Annotations.code_annotation_of_rooted annot in + let register_code_annot a state = let state_ref = ref state in ignore (Visitor.visitFramacCodeAnnotation (register state_ref) a); !state_ref diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml index 1588c2a01e597ab322f7cf4dbf235a7a4c531db8..5ef140071fc6b53abfaf0bc860bce0daab7763e7 100644 --- a/src/plugins/e-acsl/visit.ml +++ b/src/plugins/e-acsl/visit.ml @@ -333,7 +333,7 @@ class e_acsl_visitor prj generate = object (self) in let env, new_annots = Annotations.fold_code_annot - (fun _ (User old_a | AI(_, old_a)) (env, new_annots) -> + (fun _ old_a (env, new_annots) -> let a = (* [VP] Don't use Visitor here, as it will fill the queue in the middle of the computation... *)