[e-acsl] remove useless commented code

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