From c7fd9476f4dc69b326d3f97d0656f644a50293e4 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 12 May 2011 13:17:19 +0000
Subject: [PATCH] [e-acsl] remove useless commented code
---
src/plugins/e-acsl/visit.ml | 87 -------------------------------------
1 file changed, 87 deletions(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 0b4a82831c4..9791cc62cc0 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -106,94 +106,7 @@ end
(* ************************************************************************** *)
(* Environments *)
(* ************************************************************************** *)
-(*
-module New_block : sig
- val is_empty: unit -> bool
- val push: stmt -> unit
- val finalize: stmt -> block
-end = struct
-
- let stmts = ref []
-
- let push s = stmts := s :: !stmts
- let is_empty () = !stmts = []
-
- let finalize s =
- let l = s :: !stmts in
- stmts := [];
- mkBlock (List.rev l)
-
-end
-
-module New_vars: sig
-
- val push: typ -> (varinfo -> exp (* the var as exp *) -> stmt list) -> exp
- (* the closure as argument indicates how to initialize the given varinfo *)
-
- val push_and_mpz_init:
- (varinfo -> exp (* the var as exp *) -> stmt list) -> exp
- (* the closure as argument indicates how to initialize the given varinfo *)
-
- val finalize: unit -> (varinfo * exp * bool) list
-(* return the environment and reset it in order to be used again.
- Each item of the returned list contains:
- - the generated varinfo
- - a C expression corresponding to this varinfo
- - a boolean which is true iff the generated varinfo is a mpz_t variable. *)
-
-end = struct
-
- (* the finalizer resets the counter in order to keep it small. However, Cil
- visitor is dummy: it believes that my counter is its own and thus change it
- to keep it stricly growing. Too bad! :-(
-
- Could be a real issue in practice since **many** variables are generated
- for E-ACSL (at least one variable by integer constant). *)
-
- let var_cpt = ref 0
- let vlist = ref []
-
- let push_list ty mk_stmts =
- incr var_cpt;
- let is_t = Mpz.is_t ty in
- if is_t then Mpz.is_now_referenced ();
- let v =
- makeVarinfo
- ~logic:false
- ~generated:true
- false (* is a global? *)
- false (* is a formal? *)
- ("e_acsl_" ^ string_of_int !var_cpt)
- ty
- in
- let e = new_lval v in
- let stmts = mk_stmts v e in
- List.iter New_block.push stmts;
- vlist := (v, e, is_t) :: !vlist;
- e
-
- let push ty mk_stmts = push_list ty (fun v e -> mk_stmts v e)
-
- let push_and_mpz_init mk_stmts =
- push_list Mpz.t (fun v e -> Mpz.init e :: mk_stmts v e)
-
- let finalize () =
- var_cpt := 0;
- let l = !vlist in
- vlist := [];
- l
-end
-
-module New_annotations : sig
- val push: stmt -> predicate named -> unit
- val finalize : (unit -> unit) Queue.t -> unit
-end = struct
- let q = Queue.create ()
- let push s p = Queue.add (fun () -> Annotations.add_assert s [ !self ] p) q
- let finalize dest_q = Queue.transfer q dest_q
-end
- *)
module Env : sig
type t
val empty: t
--
GitLab