From 3d075af6ef25248e4baca2a2529244642cf94dd7 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 11 May 2011 13:58:20 +0000
Subject: [PATCH] [e-acsl] simplifying Visit.New_block
---
src/plugins/e-acsl/visit.ml | 13 ++++---------
1 file changed, 4 insertions(+), 9 deletions(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index a36cbbc6467..1c94e1b5f5c 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -169,21 +169,16 @@ end
module New_block : sig
val is_empty: unit -> bool
val push: stmt -> unit
- val push_at_end: stmt -> unit
val finalize: stmt -> block
end = struct
- let blist = ref []
let slist = ref []
- let push s = blist := s :: !blist
- let push_at_end s = slist := s :: !slist
-
- let is_empty () = !blist = [] && !slist = []
+ let push s = slist := s :: !slist
+ let is_empty () = !slist = []
let finalize s =
- let l = !blist @ !slist @ [ s ] in
- blist := [];
+ let l = !slist @ [ s ] in
slist := [];
mkBlock l
@@ -390,7 +385,7 @@ let rec named_predicate_to_revexp p =
let convert_named_predicate p =
let e = named_predicate_to_revexp p in
- New_block.push_at_end (mk_if e p)
+ New_block.push (mk_if e p)
let convert_annotation annot =
try
--
GitLab