[kernel] Logic_utils: optimizes the [complete_types] visitor.

Skips the visit of C codes.

src/kernel_services/ast_queries/logic_utils.ml

@@ -2349,6 +2349,15 @@ class complete_types =
              not (isLogicType Cil.isCompleteType t.term_type) ->
         ChangeDoChildrenPost({ t with term_type = v.lv_type }, fun x -> x)
       | _ -> DoChildrenPost self#insert_cast_term
+
+    method! vinst = function
+      | Code_annot _ -> Cil.DoChildren
+      | _ -> Cil.SkipChildren
+
+    method! vexpr _ = Cil.SkipChildren
+    method! vlval _ = Cil.SkipChildren
+    method! vtype _ = Cil.SkipChildren
+    method! vinit _ _ _ = Cil.SkipChildren
   end
 
 let complete_types f = Cil.visitCilFile (new complete_types) f