diff --git a/src/kernel_internals/typing/allocates.ml b/src/kernel_internals/typing/allocates.ml
index 6862e67bc672164958fbd56af4ff91629c267db0..34baf49d74397f063886726b4c6a21fa5a3e3a90 100644
--- a/src/kernel_internals/typing/allocates.ml
+++ b/src/kernel_internals/typing/allocates.ml
@@ -57,12 +57,12 @@ class vis_add_loop_allocates =
       );
       Cil.DoChildren
 
-    method! vinst _ = SkipChildren
-    method! vexpr _ = SkipChildren
-    method! vlval _ = SkipChildren
-    method! vtype _ = SkipChildren
-    method! vspec _ = SkipChildren
-    method! vcode_annot _ = SkipChildren
+    method! vinst _ = Cil.SkipChildren
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
   end
 
 let add_allocates_nothing () =
diff --git a/src/kernel_internals/typing/asm_contracts.ml b/src/kernel_internals/typing/asm_contracts.ml
index 0281d236c8435f0b70b14dde140f526197985c58..cab9b38826b22ce571d1c757bc3625d3a5f60bb7 100644
--- a/src/kernel_internals/typing/asm_contracts.ml
+++ b/src/kernel_internals/typing/asm_contracts.ml
@@ -222,11 +222,11 @@ class visit_assembly =
         Cil.SkipChildren
       | _ -> Cil.SkipChildren
 
-    method! vexpr _ = SkipChildren
-    method! vlval _ = SkipChildren
-    method! vtype _ = SkipChildren
-    method! vspec _ = SkipChildren
-    method! vcode_annot _ = SkipChildren
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
   end
 
 let transform file =
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index dca10f8fc7d60e91888192a45ddaf42523125ad9..6565c42e26b90484061688e74f20ca9fdb638c8e 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1368,8 +1368,8 @@ class canDropStmtClass pRes = object
     else
     if !pRes then DoChildren else SkipChildren
 
-  method! vinst _ = SkipChildren
-  method! vexpr _ = SkipChildren
+  method! vinst _ = Cil.SkipChildren
+  method! vexpr _ = Cil.SkipChildren
 
 end
 let canDropStatement (s: stmt) : bool =
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index 52b5692146f96e28507e53d81facbadb6e43ed79..fed8733f54f0271617cd944e3c23bb3698af4840 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -307,13 +307,13 @@ let forallStmts todo (fd : fundec) =
   let vis = object
     inherit nopCilVisitor
     method! vstmt stmt = ignore (todo stmt); DoChildren
-    method! vinst _ = SkipChildren
-    method! vexpr _ = SkipChildren
-    method! vlval _ = SkipChildren
-    method! vtype _ = SkipChildren
-    method! vspec _ = SkipChildren
-    method! vcode_annot _ = SkipChildren
-    method! vattr _ = SkipChildren
+    method! vinst _ = Cil.SkipChildren
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
+    method! vattr _ = Cil.SkipChildren
   end
   in
   ignore (visitCilFunction vis fd)
@@ -750,13 +750,13 @@ class registerLabelsVisitor : cilVisitor = object
       labels;
     DoChildren
   end
-  method! vexpr _ = SkipChildren
-  method! vtype _ = SkipChildren
-  method! vinst _ = SkipChildren
-  method! vspec _ = SkipChildren
-  method! vcode_annot _ = SkipChildren (* via Loop stmt *)
-  method! vlval _ = SkipChildren (* via UnspecifiedSequence stmt *)
-  method! vattr _ = SkipChildren (* via block stmt *)
+  method! vexpr _ = Cil.SkipChildren
+  method! vtype _ = Cil.SkipChildren
+  method! vinst _ = Cil.SkipChildren
+  method! vspec _ = Cil.SkipChildren
+  method! vcode_annot _ = Cil.SkipChildren (* via Loop stmt *)
+  method! vlval _ = Cil.SkipChildren (* via UnspecifiedSequence stmt *)
+  method! vattr _ = Cil.SkipChildren (* via block stmt *)
 end
 
 (* prepare a function for computeCFGInfo by removing break, continue,
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 1b448c946391315e745afb784c02606c32ac6630..8b515e1324e0a864d89e8defac41540c51606e0a 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -3232,7 +3232,7 @@ let find_decls g =
       method! vlogic_var_decl lv =
         res := Cil_datatype.Logic_var.Set.add lv !res;
         SkipChildren
-      method! vspec _ = SkipChildren
+      method! vspec _ = Cil.SkipChildren
       method! vfunc f =
         ignore (self#vvdec f.svar);
         Option.iter (ignore $ self#vlogic_var_decl) f.svar.vlogic_var_assoc;
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 83a59cde83fddd66975eea7b3d8834ccea9ae4b9..3b3eaadd34889a78bfab20890733789dd0e0e407 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -663,8 +663,8 @@ class markReferencedVisitor = object (self)
     end;
     SkipChildren
 
-  method! vspec _ = SkipChildren
-  method! vcode_annot _ = SkipChildren
+  method! vspec _ = Cil.SkipChildren
+  method! vcode_annot _ = Cil.SkipChildren
 end
 
 let markReferenced ast =
@@ -748,8 +748,8 @@ class markUsedLabels is_removable (labelMap: (string, unit) Hashtbl.t) =
       DoChildren
 
     (* No need to go into expressions or types *)
-    method! vexpr _ = SkipChildren
-    method! vtype _ = SkipChildren
+    method! vexpr _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
   end
 
 class removeUnusedLabels is_removable (labelMap: (string, unit) Hashtbl.t) = object
@@ -768,9 +768,9 @@ class removeUnusedLabels is_removable (labelMap: (string, unit) Hashtbl.t) = obj
     DoChildren
 
   (* No need to go into expressions or instructions *)
-  method! vexpr _ = SkipChildren
-  method! vinst _ = SkipChildren
-  method! vtype _ = SkipChildren
+  method! vexpr _ = Cil.SkipChildren
+  method! vinst _ = Cil.SkipChildren
+  method! vtype _ = Cil.SkipChildren
 end
 
 (***********************************************************************
diff --git a/src/kernel_internals/typing/substitute_const_globals.ml b/src/kernel_internals/typing/substitute_const_globals.ml
index d9ba1dcc88cfbdb3006ef40101abd4dfd0837660..20766da3dc6ccedb18d64975679babb2733aed3c 100644
--- a/src/kernel_internals/typing/substitute_const_globals.ml
+++ b/src/kernel_internals/typing/substitute_const_globals.ml
@@ -105,9 +105,9 @@ class constGlobSubstVisitorClass : cilVisitor = object
     | _ ->
       DoChildren
 
-  method! vtype _ = SkipChildren
-  method! vspec _ = SkipChildren
-  method! vcode_annot _ = SkipChildren
+  method! vtype _ = Cil.SkipChildren
+  method! vspec _ = Cil.SkipChildren
+  method! vcode_annot _ = Cil.SkipChildren
 end
 
 let constGlobSubstVisitor = new constGlobSubstVisitorClass
diff --git a/src/kernel_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index 4ebac5d58b904bbf9f88bb7ba3e01eeec30554fb..bc475d5d55640120e8f8f589573d19685974bb8b 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -151,12 +151,12 @@ let update_gotos sid_tbl block =
           DoChildren
         | _ -> DoChildren
       (* speed up: skip non interesting subtrees *)
-      method! vvdec _ = SkipChildren (* via visitCilFunction *)
-      method! vspec _ = SkipChildren (* via visitCilFunction *)
-      method! vcode_annot _ = SkipChildren (* via Code_annot stmt *)
-      method! vexpr _ = SkipChildren (* via stmt such as Return, IF, ... *)
-      method! vlval _ = SkipChildren (* via stmt such as Set, Call, Asm, ... *)
-      method! vattr _ = SkipChildren (* via Asm stmt *)
+      method! vvdec _ = Cil.SkipChildren (* via visitCilFunction *)
+      method! vspec _ = Cil.SkipChildren (* via visitCilFunction *)
+      method! vcode_annot _ = Cil.SkipChildren (* via Code_annot stmt *)
+      method! vexpr _ = Cil.SkipChildren (* via stmt such as Return, IF, ... *)
+      method! vlval _ = Cil.SkipChildren (* via stmt such as Set, Call, Asm, ... *)
+      method! vattr _ = Cil.SkipChildren (* via Asm stmt *)
     end
   in visitCilBlock (goto_updater:>cilVisitor) block
 
@@ -710,12 +710,12 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
 
     | _ -> DoChildren
 
-  method! vinst _ = SkipChildren
-  method! vexpr _ = SkipChildren
-  method! vlval _ = SkipChildren
-  method! vtype _ = SkipChildren
-  method! vspec _ = SkipChildren
-  method! vcode_annot _ = SkipChildren
+  method! vinst _ = Cil.SkipChildren
+  method! vexpr _ = Cil.SkipChildren
+  method! vlval _ = Cil.SkipChildren
+  method! vtype _ = Cil.SkipChildren
+  method! vspec _ = Cil.SkipChildren
+  method! vcode_annot _ = Cil.SkipChildren
 end
 
 (* Performs unrolling transformation without using -ulevel option.
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index 5adfcc1b04d46ee3b924cd6b4ef3701d6d3de1f7..896aba7478862d45596a3a923f34e744ab690110 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -65,12 +65,12 @@ class all_exn =
         all_exn <- Cil_datatype.Typ.Set.add (purify t) all_exn;
         SkipChildren
       | _ -> DoChildren
-    method! vinst _ = SkipChildren
-    method! vexpr _ = SkipChildren
-    method! vlval _ = SkipChildren
-    method! vtype _ = SkipChildren
-    method! vspec _ = SkipChildren
-    method! vcode_annot _ = SkipChildren
+    method! vinst _ = Cil.SkipChildren
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
   end
 
 let compute_all_exn () =
@@ -265,11 +265,11 @@ class exn_visit =
       in
       DoChildrenPost after_visit
 
-    method! vexpr _ = SkipChildren
-    method! vlval _ = SkipChildren
-    method! vtype _ = SkipChildren
-    method! vspec _ = SkipChildren
-    method! vcode_annot _ = SkipChildren
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
   end
 
 let compute_kf kf =
diff --git a/src/kernel_services/analysis/undefined_sequence.ml b/src/kernel_services/analysis/undefined_sequence.ml
index ef71fa89e876a5330a637a724f741c600122df38..f70f8043e1809d0f15cc89191826c4cb98b13254 100644
--- a/src/kernel_services/analysis/undefined_sequence.ml
+++ b/src/kernel_services/analysis/undefined_sequence.ml
@@ -144,12 +144,12 @@ let check_sequences file =
        | _ -> ());
       Cil.DoChildren
 
-    method! vinst _ = SkipChildren
-    method! vexpr _ = SkipChildren
-    method! vlval _ = SkipChildren
-    method! vtype _ = SkipChildren
-    method! vspec _ = SkipChildren
-    method! vcode_annot _ = SkipChildren
+    method! vinst _ = Cil.SkipChildren
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
   end
   in
   Cil.visitCilFileFunctions check_unspec file
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index 14f9ade3b3b2add5e0bb8ca88a8949a6139ed5da..ec88837490f29c1a8de2b3d12c72e8bc50dad5e6 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -153,12 +153,12 @@ let compute () =
                   Cil_datatype.Varinfo.pretty fd.svar)
            | GVar _ -> Cil.SkipChildren
            | _ -> Cil.SkipChildren
-         method! vinst _ = SkipChildren
-         method! vexpr _ = SkipChildren
-         method! vlval _ = SkipChildren
-         method! vtype _ = SkipChildren
-         method! vspec _ = SkipChildren
-         method! vcode_annot _ = SkipChildren
+         method! vinst _ = Cil.SkipChildren
+         method! vexpr _ = Cil.SkipChildren
+         method! vlval _ = Cil.SkipChildren
+         method! vtype _ = Cil.SkipChildren
+         method! vspec _ = Cil.SkipChildren
+         method! vcode_annot _ = Cil.SkipChildren
        end
        in
        Cil.visitCilFile (visitor :> Cil.cilVisitor) p;
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index eefaadb83fee396f58195c7f4bf5804d08243135..b64a9a308b067bf8ccb10ac22b1d455375f58d22 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1006,12 +1006,12 @@ let cleanup file =
              Cfg.computeFileCFG f; f end
             else f)
 
-    method! vinst _ = SkipChildren
-    method! vexpr _ = SkipChildren
-    method! vlval _ = SkipChildren
-    method! vtype _ = SkipChildren
-    method! vspec _ = SkipChildren
-    method! vcode_annot _ = SkipChildren
+    method! vinst _ = Cil.SkipChildren
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
   end
   in visitFramacFileSameGlobals visitor file
 
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index 26b04df7a4c0053de29dcae93544d1f9c8bd48e8..53fc32ff9326cebf312c641f686e9e06ab34f1af 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -382,7 +382,7 @@ end = struct
       in
       DoChildrenPost do_post
 
-    (*method vvdec _ = SkipChildren (* everything is done elsewhere *)*)
+    (*method vvdec _ = Cil.SkipChildren (* everything is done elsewhere *)*)
 
     method private add_formals_bindings v formals =
       Varinfo.Hashtbl.add formals_table v formals
diff --git a/src/kernel_services/ast_transformations/inline.ml b/src/kernel_services/ast_transformations/inline.ml
index 3a3739578a46efacdff8f39271f69dba00faefb3..db1d1074e643aeaa9a55a334db4f94605f4b78b9 100644
--- a/src/kernel_services/ast_transformations/inline.ml
+++ b/src/kernel_services/ast_transformations/inline.ml
@@ -342,11 +342,11 @@ let inliner functions_to_inline = object (self)
          let kf = Globals.Functions.get f.svar in
          already_visited <- Cil_datatype.Kf.Set.add kf functions_to_inline; f)
 
-  method! vexpr _ = SkipChildren
-  method! vlval _ = SkipChildren
-  method! vtype _ = SkipChildren
-  method! vspec _ = SkipChildren
-  method! vcode_annot _ = SkipChildren
+  method! vexpr _ = Cil.SkipChildren
+  method! vlval _ = Cil.SkipChildren
+  method! vtype _ = Cil.SkipChildren
+  method! vspec _ = Cil.SkipChildren
+  method! vcode_annot _ = Cil.SkipChildren
 end
 
 let remove_local_statics = object
diff --git a/src/plugins/metrics/metrics_pivot.ml b/src/plugins/metrics/metrics_pivot.ml
index 3f4b86ef18546b3486c2a1cb907645e7b17059d0..2f943abca822231740f08df2e923ac6a2e532022 100644
--- a/src/plugins/metrics/metrics_pivot.ml
+++ b/src/plugins/metrics/metrics_pivot.ml
@@ -314,17 +314,17 @@ class full_visitor = object(self)
   method add_annot ?names node =
     self#add ~node ?names (Syntax Annotation)
 
-  method! vvrbl (_v:varinfo) = DoChildren
-  method! vvdec (_v:varinfo) = DoChildren
-  method! vexpr (_e:exp) = DoChildren
-  method! vlval (_l:lval) = DoChildren
-  method! voffs (_o:offset) = DoChildren
-  method! vinitoffs (_o:offset) = DoChildren
+  method! vvrbl (_v:varinfo) = Cil.DoChildren
+  method! vvdec (_v:varinfo) = Cil.DoChildren
+  method! vexpr (_e:exp) = Cil.DoChildren
+  method! vlval (_l:lval) = Cil.DoChildren
+  method! voffs (_o:offset) = Cil.DoChildren
+  method! vinitoffs (_o:offset) = Cil.DoChildren
 
   method! vinst (i:instr) =
     let node = node_of_instr i in
     self#add_code node;
-    DoChildren
+    Cil.DoChildren
 
   method! vstmt (s:stmt) =
     begin
@@ -332,7 +332,7 @@ class full_visitor = object(self)
       | None -> ()
       | Some node -> self#add_code node
     end;
-    DoChildren
+    Cil.DoChildren
 
   method! vfunc (f:fundec) =
     cur_func <- Some f.svar.vname;
@@ -349,52 +349,52 @@ class full_visitor = object(self)
       self#add_decl ~func ~names node
     else
       self#add_code ~func ~names node;
-    DoChildren
-
-  method! vblock _ = DoChildren
-  method! vinit _ _ _ = DoChildren
-  method! vlocal_init _ _ = DoChildren
-  method! vtype _ = DoChildren
-  method! vcompinfo _ = DoChildren
-  method! venuminfo _ = DoChildren
-  method! vfieldinfo _ = DoChildren
-  method! venumitem _ = DoChildren
-  method! vattr _ = DoChildren
-  method! vattrparam _ = DoChildren
-  method! vmodel_info _ = DoChildren
-  method! vlogic_type _ = DoChildren
-  method! videntified_term _ = DoChildren
-  method! vterm _ = DoChildren
-  method! vterm_node _ = DoChildren
-  method! vterm_lval _ = DoChildren
-  method! vterm_lhost _ = DoChildren
-  method! vterm_offset _ = DoChildren
-  method! vlogic_label _ = DoChildren
-  method! vlogic_info_decl _ = DoChildren
-  method! vlogic_info_use _ = DoChildren
-  method! vlogic_type_info_decl _ = DoChildren
-  method! vlogic_type_info_use _ = DoChildren
-  method! vlogic_type_def _ = DoChildren
-  method! vlogic_ctor_info_decl _ = DoChildren
-  method! vlogic_ctor_info_use _ = DoChildren
-  method! vlogic_var_use _ = DoChildren
-  method! vlogic_var_decl _ = DoChildren
-  method! vquantifiers _ = DoChildren
+    Cil.DoChildren
+
+  method! vblock _ = Cil.DoChildren
+  method! vinit _ _ _ = Cil.DoChildren
+  method! vlocal_init _ _ = Cil.DoChildren
+  method! vtype _ = Cil.DoChildren
+  method! vcompinfo _ = Cil.DoChildren
+  method! venuminfo _ = Cil.DoChildren
+  method! vfieldinfo _ = Cil.DoChildren
+  method! venumitem _ = Cil.DoChildren
+  method! vattr _ = Cil.DoChildren
+  method! vattrparam _ = Cil.DoChildren
+  method! vmodel_info _ = Cil.DoChildren
+  method! vlogic_type _ = Cil.DoChildren
+  method! videntified_term _ = Cil.DoChildren
+  method! vterm _ = Cil.DoChildren
+  method! vterm_node _ = Cil.DoChildren
+  method! vterm_lval _ = Cil.DoChildren
+  method! vterm_lhost _ = Cil.DoChildren
+  method! vterm_offset _ = Cil.DoChildren
+  method! vlogic_label _ = Cil.DoChildren
+  method! vlogic_info_decl _ = Cil.DoChildren
+  method! vlogic_info_use _ = Cil.DoChildren
+  method! vlogic_type_info_decl _ = Cil.DoChildren
+  method! vlogic_type_info_use _ = Cil.DoChildren
+  method! vlogic_type_def _ = Cil.DoChildren
+  method! vlogic_ctor_info_decl _ = Cil.DoChildren
+  method! vlogic_ctor_info_use _ = Cil.DoChildren
+  method! vlogic_var_use _ = Cil.DoChildren
+  method! vlogic_var_decl _ = Cil.DoChildren
+  method! vquantifiers _ = Cil.DoChildren
   method! videntified_predicate _ =
     (* should be done by the annotations visitor *)
     assert false
-  method! vpredicate_node _ = DoChildren
-  method! vpredicate _ = DoChildren
-  method! vbehavior _ = DoChildren
-  method! vassigns _ = DoChildren
-  method! vfrees _ = DoChildren
-  method! vallocates _ = DoChildren
-  method! vallocation _ = DoChildren
-  method! vloop_pragma _ = DoChildren
-  method! vslice_pragma _ = DoChildren
-  method! vimpact_pragma _ = DoChildren
-  method! vdeps _ = DoChildren
-  method! vfrom _ = DoChildren
+  method! vpredicate_node _ = Cil.DoChildren
+  method! vpredicate _ = Cil.DoChildren
+  method! vbehavior _ = Cil.DoChildren
+  method! vassigns _ = Cil.DoChildren
+  method! vfrees _ = Cil.DoChildren
+  method! vallocates _ = Cil.DoChildren
+  method! vallocation _ = Cil.DoChildren
+  method! vloop_pragma _ = Cil.DoChildren
+  method! vslice_pragma _ = Cil.DoChildren
+  method! vimpact_pragma _ = Cil.DoChildren
+  method! vdeps _ = Cil.DoChildren
+  method! vfrom _ = Cil.DoChildren
   method! vcode_annot _ =
     (* should be done by the annotations visitor *)
     assert false
@@ -402,7 +402,7 @@ class full_visitor = object(self)
     let node = node_of_global_annotation ga in
     let names = Option.to_list (name_of_global_annotation ga) in
     self#add_annot ~names node;
-    DoChildren
+    Cil.DoChildren
 end
 
 let ca_visitor_cur_func : string option ref = ref None
@@ -420,18 +420,18 @@ class code_annot_visitor = object(self)
   method! videntified_predicate {ip_content = {tp_kind}} =
     let node = node_of_predicate_kind tp_kind in
     self#add_annot node;
-    DoChildren
+    Cil.DoChildren
 
   method! vcode_annot ca =
     let content = ca.annot_content in
     self#add_annot (node_of_code_annotation_node content);
-    DoChildren
+    Cil.DoChildren
 
   method! vannotation ga =
     let node = node_of_global_annotation ga in
     let names = Option.to_list (name_of_global_annotation ga) in
     self#add_annot ~names node;
-    DoChildren
+    Cil.DoChildren
 end
 
 let visit_annots () =
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 55241baccf115f201dc45a7fc07f990e3c3f2349..dc71060c5f2182ada0acb15ebdbb0cbd789654c0 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -96,12 +96,12 @@ let mark_unreachable () =
       end;
       Cil.DoChildren
 
-    method! vinst _ = SkipChildren
-    method! vexpr _ = SkipChildren
-    method! vlval _ = SkipChildren
-    method! vtype _ = SkipChildren
-    method! vspec _ = SkipChildren
-    method! vcode_annot _ = SkipChildren
+    method! vinst _ = Cil.SkipChildren
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
   end
   in
   Annotations.iter_all_code_annot do_code_annot;
diff --git a/src/plugins/value/partitioning/split_return.ml b/src/plugins/value/partitioning/split_return.ml
index e2bbd2b7612c2cce1437d543895c5b7e2490d4cd..bccdc17b6ffb533e0b129deac52dfe8bb43439c2 100644
--- a/src/plugins/value/partitioning/split_return.ml
+++ b/src/plugins/value/partitioning/split_return.ml
@@ -209,9 +209,9 @@ module ReturnUsage = struct
     method result () =
       summarize_by_lv usage
 
-    method! vtype _ = SkipChildren
-    method! vspec _ = SkipChildren
-    method! vcode_annot _ = SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vspec _ = Cil.SkipChildren
+    method! vcode_annot _ = Cil.SkipChildren
   end
 
   (* For functions returning pointers, add a split on NULL/non-NULL *)
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index f0adcba3d16e439c27a3156fffe50c62f1282f7f..5ae5facb3291b03dc97358412d70ea07e83a1b7d 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -421,7 +421,7 @@ class visitor =
       | Dextended _
         -> SkipChildren
 
-    method! vfunc _ = SkipChildren
+    method! vfunc _ = Cil.SkipChildren
 
   end