[E-ACSL] compatibility with warning 7

src/plugins/e-acsl/pre_analysis.ml

@@ -27,7 +27,7 @@ let init_mpz () =
   Options.feedback ~level:2 "initializing GMP type.";
   let set_mpzt = object
     inherit Cil.nopCilVisitor
-    method vglob = function
+    method !vglob = function
     | GType({ torig_name = s } as info, _) when s = "mpz_t" ->
       Mpz.set_t info;
       Cil.SkipChildren
@@ -313,7 +313,7 @@ module rec Transfer
 
   let register_object kf state_ref = object
     inherit Visitor.frama_c_inplace
-    method vpredicate = function
+    method !vpredicate = function
     | Pvalid(_, t) | Pvalid_read(_, t) | Pinitialized(_, t) ->
       (*	Options.feedback "REGISTER %a" Cil.d_term t;*)
       state_ref := register_term kf !state_ref t;
@@ -326,7 +326,7 @@ module rec Transfer
     | Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _ 
     | Plet _ | Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
       Cil.DoChildren
-    method vterm term = match term.term_node with
+    method !vterm term = match term.term_node with
     | Tbase_addr(_, t) | Toffset(_, t) | Tblock_length(_, t) ->
       state_ref := register_term kf !state_ref t;
       Cil.DoChildren
@@ -341,8 +341,8 @@ module rec Transfer
     | Tcomprehension _ | Trange _ | Tlet _ | TLogic_coerce _ -> 
       (* potential sub-term inside *)
       Cil.DoChildren
-    method vlogic_label _ = Cil.SkipChildren
-    method vterm_lhost = function
+    method !vlogic_label _ = Cil.SkipChildren
+    method !vterm_lhost = function
     | TMem t ->
       (* potential RTE *)
       state_ref := register_term kf !state_ref t;

src/plugins/e-acsl/pre_visit.ml

@@ -103,7 +103,7 @@ let dup_funspec tbl bhv spec =
 
     val already_visited = Cil_datatype.Logic_var.Hashtbl.create 7
 
-    method vlogic_info_use li =
+    method !vlogic_info_use li =
       if Global.mem_logic_info li then
 	Cil.ChangeDoChildrenPost
 	  ({ li with l_var_info = li.l_var_info } (* force a copy *),
@@ -111,7 +111,7 @@ let dup_funspec tbl bhv spec =
       else
 	Cil.JustCopy
 
-    method vterm_offset _ =
+    method !vterm_offset _ =
       Cil.DoChildrenPost
 	(function
 	(* no way to directly visit fieldinfo and model_info uses *)	
@@ -119,7 +119,7 @@ let dup_funspec tbl bhv spec =
 	| TModel(mi, off) -> TModel(Cil.get_model_info bhv mi, off)
 	| off -> off)
 
-    method vlogic_var_use orig_lvi =
+    method !vlogic_var_use orig_lvi =
       match orig_lvi.lv_origin with
       | None -> 
 	Cil.JustCopy
@@ -149,10 +149,10 @@ let dup_funspec tbl bhv spec =
 		 assert vi.vglob;
 		 Cil.get_logic_var bhv lvi)
 
-    method videntified_term _ = 
+    method !videntified_term _ = 
       Cil.DoChildrenPost Logic_const.refresh_identified_term
 
-    method videntified_predicate _ = 
+    method !videntified_predicate _ = 
       Cil.DoChildrenPost Logic_const.refresh_predicate
   end in
   Cil.visitCilFunspec o spec
@@ -249,7 +249,7 @@ class dup_functions_visitor prj = object (self)
     | Memory_model -> before_memory_model <- Code
     | Code -> ()
 
-  method vcode_annot a =
+  method !vcode_annot a =
     Cil.JustCopyPost
       (fun a' ->
 	let get_ppt kf stmt a = Property.ip_of_code_annot kf stmt a in
@@ -264,11 +264,11 @@ class dup_functions_visitor prj = object (self)
 	     a');
 	a')
 
-  method vlogic_info_decl li = 
+  method !vlogic_info_decl li = 
     Global.add_logic_info li;
     Cil.JustCopy
 
-  method vvrbl vi =
+  method !vvrbl vi =
     try
       let new_vi = Cil_datatype.Varinfo.Hashtbl.find fct_tbl vi in
       Cil.ChangeTo new_vi
@@ -280,7 +280,7 @@ class dup_functions_visitor prj = object (self)
     | TFun(_, _, variadic, _) -> not variadic
     | _ -> false
 
-  method vglob_aux = function
+  method !vglob_aux = function
   | GVarDecl(_, vi, loc) | GFun({ svar = vi }, loc)
       when self#is_unvariadic_function vi
 	&& not (Misc.is_library_loc loc) 
@@ -346,7 +346,7 @@ if there are memory-related annotations.@]"
     self#next ();
     Cil.DoChildrenPost self#insert_libc
 
-  method vfile _ =
+  method !vfile _ =
     Cil.DoChildrenPost
       (fun f ->
 	match libc_decls with

src/plugins/e-acsl/translate.ml

@@ -466,7 +466,7 @@ and at_to_exp env t_opt label e =
     let res = ref false in
     let o = object
       inherit Cil.nopCilVisitor
-      method vlval (host, _) = match host with
+      method !vlval (host, _) = match host with
       | Var v -> 
 	if Pre_analysis.old_must_model_vi (Env.get_behavior env) v then 
 	  res := true;
@@ -495,7 +495,7 @@ and at_to_exp env t_opt label e =
      one). *)
   let o = object 
     inherit Visitor.frama_c_inplace
-    method vstmt_aux stmt = 
+    method !vstmt_aux stmt = 
       (* either a standard C affectation or an mpz one according to type of
 	 [e] *) 
       let new_stmt = Mpz.init_set ~loc (Cil.var res_v) res e in

src/plugins/e-acsl/visit.ml

@@ -36,7 +36,7 @@ let move_labels env stmt new_stmt =
     (* update the gotos of the function jumping to one of the labels *)
     let o = object 
       inherit Visitor.frama_c_inplace
-      method vstmt_aux s = match s.skind with
+      method !vstmt_aux s = match s.skind with
       | Goto(s_ref, _) -> 
 	(* [!s_ref] and [stmt] are not part of the same project, thus it
 	   is safer to compare the ids than to use Stmt.equal *)
@@ -45,10 +45,10 @@ let move_labels env stmt new_stmt =
       | _ -> Cil.DoChildren
       (* improve efficiency: skip childrens of vstmt which cannot
 	 contain any stmt *)
-      method vinst _ = Cil.SkipChildren
-      method vexpr _ = Cil.SkipChildren
-      method vcode_annot _ = Cil.SkipChildren
-      method vlval _ = Cil.SkipChildren
+      method !vinst _ = Cil.SkipChildren
+      method !vexpr _ = Cil.SkipChildren
+      method !vcode_annot _ = Cil.SkipChildren
+      method !vlval _ = Cil.SkipChildren
     end in
     let vis = Env.get_visitor env in
     let f = Extlib.the vis#current_func in
@@ -114,7 +114,7 @@ class e_acsl_visitor prj generate = object (self)
   method private reset_env () =
     function_env := Env.empty (self :> Visitor.frama_c_visitor)
 
-  method vfile _f =
+  method !vfile _f =
     (* copy the options used during the visit in the new project: it is the
        right place to do this: it is still before visiting, but after
        that the visitor internals reset all of them :-(. *)
@@ -240,7 +240,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
 	if generate then Project.clear ~selection ~project:prj ();
 	f)
 
-  method vglob_aux = function
+  method !vglob_aux = function
   | GVarDecl(_, vi, _) | GVar(vi, _, _) | GFun({ svar = vi }, _) 
       when Misc.is_library_loc vi.vdecl ->
     if generate then
@@ -292,7 +292,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
     if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
     else Cil.DoChildren
 
-  method vinit vi _off _i = 
+  method !vinit vi _off _i = 
     if generate then
       if Pre_analysis.must_model_vi vi then begin
 	keep_initializer <- Some true;
@@ -308,7 +308,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
     else
       Cil.SkipChildren
 
-  method vvdec vi = 
+  method !vvdec vi = 
     try
       let old_vi = Cil.get_original_varinfo self#behavior vi in
       let old_kf = Globals.Functions.get old_vi in
@@ -332,7 +332,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
       body.blocals
       vars
 
-  method vfunc f =
+  method !vfunc f =
     if generate then
       let kf = Extlib.the self#current_kf in
       Options.feedback ~dkey ~level:2 "entering in function %a." 
@@ -378,7 +378,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
     let env_ref = ref env in
     let o = object
       inherit Cil.genericCilVisitor (Cil.copy_visit (Project.current ()))
-      method vexpr e = match e.enode with
+      method !vexpr e = match e.enode with
       | Const(CStr s) ->
 	let loc = e.eloc in
 	let _, exp, env = 
@@ -405,7 +405,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
     let e = Cil.visitCilExpr o e in
     e, !env_ref
 
-  method vstmt_aux stmt =
+  method !vstmt_aux stmt =
     Options.debug ~level:4 "proceeding stmt (sid %d) %a@." 
       stmt.sid Stmt.pretty stmt;
     let kf = Extlib.the self#current_kf in
@@ -572,7 +572,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
       function_env := Env.add_stmt !function_env stmt
     end
 
-  method vinst = function
+  method !vinst = function
   | Set(old_lv, _, _) ->
     if generate then
       Cil.DoChildrenPost 
@@ -596,7 +596,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
   | _ ->
     Cil.DoChildren
 
-  method vblock blk =
+  method !vblock blk =
     let handle_memory new_blk = 
       match new_blk.blocals with
       | [] -> new_blk
@@ -644,7 +644,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
     in
     if generate then Cil.DoChildrenPost handle_memory else Cil.DoChildren
 
-  method vexpr exp = 
+  method !vexpr exp = 
     if generate then
       match keep_initializer with
       | Some false -> Cil.JustCopy