[kernel] New function 'has_definition' in Kernel_function

src/kernel_internals/typing/ghost_accesses.ml

@@ -73,10 +73,6 @@ module Error = struct
       "Call via a function pointer cannot be checked" ;
 end
 
-let has_definition kf =
-  try ignore (Kernel_function.get_definition kf) ; true
-  with Kernel_function.No_Definition -> false
-
 let is_ret_var vi =
   String.equal vi.vorig_name "__retres"
 
@@ -129,7 +125,9 @@ class visitor = object(self)
       let post g = self#reset_loc() ; g in
 
       let kf = Globals.Functions.get vi in
-      if vi.vghost && vi.vreferenced && not (has_definition kf) then begin
+      if vi.vghost && vi.vreferenced
+         && not (Kernel_function.has_definition kf)
+      then begin
         let spec = try Annotations.funspec ~populate:false kf
           with _ -> empty_funspec ()
         in
@@ -227,7 +225,8 @@ class visitor = object(self)
       let kf = Extlib.the (self#current_kf) in
       match assigns with
       | Writes froms -> List.iter check_assign froms
-      | WritesAny when not (has_definition kf) -> self#bad_ghost_function kf
+      | WritesAny when not (Kernel_function.has_definition kf) ->
+        self#bad_ghost_function kf
       | WritesAny ->
         (* Even without assigns, a definition is enough to check that the
            function does not assigns non-ghost locations. *)

src/kernel_services/ast_data/kernel_function.ml

@@ -71,6 +71,9 @@ exception No_Definition
 let get_definition kf = match kf.fundec with
   | Definition (f,_) -> f
   | Declaration _ -> raise No_Definition
+let has_definition kf = match kf.fundec with
+  | Definition  _ -> true
+  | Declaration _ -> false
 
 (* ************************************************************************* *)
 (** {2 Kernel functions are comparable} *)
@@ -308,7 +311,7 @@ let stmt_in_loop kf stmt =
     val is_in_loop = Stack.create ()
     method! vstmt s =
       match s.skind with
-        | Loop _ -> 
+        | Loop _ ->
           Stack.push true is_in_loop;
           if Cil_datatype.Stmt.equal s stmt then raise (Res.Found true);
           Cil.DoChildrenPost (fun s -> ignore (Stack.pop is_in_loop); s)
@@ -442,7 +445,7 @@ let find_label kf label =
   Datatype.String.Map.find label labels
 
 let get_called fct = match fct.enode with
-  | Lval (Var vkf, NoOffset) -> 
+  | Lval (Var vkf, NoOffset) ->
       (try Some (Globals.Functions.get vkf)
        with Not_found -> None)
   | _ -> None

src/kernel_services/ast_data/kernel_function.mli

@@ -86,7 +86,7 @@ val find_from_sid : int -> stmt * t
 
 val find_englobing_kf : stmt -> t
   (** @return the function to which the statement belongs. Same
-      complexity as [find_from_sid] 
+      complexity as [find_from_sid]
       @raise Not_found if the given statement is not correctly registered *)
 
 val find_enclosing_block: stmt -> block
@@ -227,6 +227,9 @@ exception No_Definition
 val get_definition : t -> fundec
   (** @raise No_Definition if the given function is not a definition.
       @plugin development guide *)
+val has_definition : t -> bool
+  (** @return [true] iff the given kernel function has a defintion.
+      @since Frama-C+dev *)
 
 (* ************************************************************************* *)
 (** {2 Membership of variables} *)