From 78b39b3173eb222cf5bfaf8db00e9fe76cdf783b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 13 May 2011 14:39:01 +0000
Subject: [PATCH] [e-acsl] a little bit more permissive for preconditions

---
 src/plugins/e-acsl/TODO     | 1 +
 src/plugins/e-acsl/visit.ml | 4 +++-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index c56fe8cb776..804a82b6159 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -16,6 +16,7 @@
 #########
 
 - tester les opérations binaires sur les pointeurs (requiert complex left value)
+- tester plusieurs fonctions contenant des annotations
 - améliorer test "integer_constant.i" quand bug fixed #745
 - améliorer test "arith.i" quand bug fixed #751
 
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 94504c62f46..d7383514c0d 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -473,7 +473,9 @@ let rec named_predicate_to_exp env p =
 (* ************************************************************************** *)
 
 let convert_preconditions _only_behaviors env _funspec behaviors =
-  if behaviors <> [] then not_yet "requires of behaviors";
+  List.iter
+    (fun b -> if b.b_requires <> [] then not_yet "requires of behaviors")
+    behaviors;
   let p = Logic_const.ptrue in
   let e, env = named_predicate_to_exp env p in
   p, e, env
-- 
GitLab