optimize Gmp.init_t a bit

src/plugins/e-acsl/gmp.ml

@@ -77,19 +77,30 @@ module Q = Make(struct end)
 
 let init_t () =
   Options.feedback ~level:2 "initializing GMP types.";
-  let set_mp_t = object
+  let set_mp_t = object (self)
     inherit Cil.nopCilVisitor
+
+    (* exit after having initialized both Z.t and Q.t *)
+    val mutable visited = false
+    method private set f info =
+      f info;
+      if visited then
+        raise Exit
+      else begin
+        visited <- true;
+        Cil.SkipChildren
+      end
+
     method !vglob = function
     | GType({ torig_name = s } as info, _) when s = "__e_acsl_mpz_t" ->
-      Z.set_t info;
-      Cil.SkipChildren
+      self#set Z.set_t info
     | GType({ torig_name = s } as info, _) when s = "__e_acsl_mpq_t" ->
-      Q.set_t info;
-      Cil.SkipChildren
+      self#set Q.set_t info
     | _ ->
       Cil.SkipChildren
+
   end in
-  Cil.visitCilFileSameGlobals set_mp_t (Ast.get ())
+  try Cil.visitCilFileSameGlobals set_mp_t (Ast.get ()) with Exit -> ()
 
 (**************************************************************************)
 (************************* Calls to builtins ******************************)

src/plugins/e-acsl/loops.ml

@@ -309,7 +309,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     let stmts, env =
       mk_nested_loops ~loc mk_innermost_block kf env lscope_vars'
     in
-    (* remove logic binding now that the block is constructed *)
+    (* remove the logic binding now that the block is constructed *)
     Env.Logic_binding.remove env lv;
     (* return *)
     let_stmt :: stmts, env