From cc7c4a2d5513aecdda48362d2fa6da0dcdefa104 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 5 Nov 2012 16:34:57 +0000
Subject: [PATCH] [E-ACSL] update according to kernel's changes
---
src/plugins/e-acsl/pre_analysis.ml | 3 +--
src/plugins/e-acsl/visit.ml | 2 +-
2 files changed, 2 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index da3c224a4f0..caa9aa30249 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 1588c2a01e5..5ef140071fc 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... *)
--
GitLab