diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 94be68f46f229218626cd984f50d41fd1bad28f6..ae7aef2e3c2d93304090e54e40b9e78f1b53f7e2 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5992,14 +5992,19 @@ let rec have_compatible_qualifiers_deep ?(context=Identical) t1 t2 =
   | _, _ -> included_qualifiers ~context (typeAttrs t1) (typeAttrs t2)
 
 
+let rec is_nullptr e =
+  match e.enode with
+  | Const (CInt64 (i,_,_)) -> Integer.is_zero i
+  | CastE (t,e) when isPointerType t -> is_nullptr e
+  | _ -> false
+
 (* true if the expression is known to be a boolean result, i.e. 0 or 1. *)
 let rec is_boolean_result e =
   (isBoolType (typeOf e)) ||
   match e.enode with
   | Const _ ->
     (match isInteger e with
-     | Some i ->
-       Integer.equal i Integer.zero || Integer.equal i Integer.one
+     | Some i -> Integer.is_zero i || Integer.is_one i
      | None -> false)
   | CastE (_, e) -> is_boolean_result e
   | BinOp ((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr), _, _, _) -> true
@@ -6301,8 +6306,7 @@ let areCompatibleTypes ?strictReturnTypes ?context t1 t2 =
 
 (******************** CASTING *****)
 
-
-let checkCast ?context ?(fromsource=false) =
+let checkCast ?context ?(nullptr_cast=false) ?(fromsource=false) =
   let rec default_rec oldt newt =
     let dkey = Kernel.dkey_typing_cast in
     let error s =
@@ -6402,16 +6406,17 @@ let checkCast ?context ?(fromsource=false) =
     (* No other conversion implying a pointer to function
           and a pointer to object are supported. *)
     | TPtr (t1, _), TPtr (t2, _) when isFunctionType t1 && isObjectType t2 ->
-      Kernel.warning
-        ~wkey:Kernel.wkey_incompatible_pointer_types
-        ~current:true
-        "casting function to %a" Cil_datatype.Typ.pretty newt
+      if not nullptr_cast then
+        Kernel.warning
+          ~wkey:Kernel.wkey_incompatible_pointer_types
+          ~current:true
+          "casting function to %a" Cil_datatype.Typ.pretty newt
     | TPtr (t1, _), TPtr (t2, _) when isFunctionType t2 && isObjectType t1 ->
-      Kernel.warning
-        ~wkey:Kernel.wkey_incompatible_pointer_types
-        ~current:true
-        "casting function from %a" Cil_datatype.Typ.pretty oldt
-
+      if not nullptr_cast then
+        Kernel.warning
+          ~wkey:Kernel.wkey_incompatible_pointer_types
+          ~current:true
+          "casting function from %a" Cil_datatype.Typ.pretty oldt
 
     | _, TPtr (t1, _) when isFunctionType t1 ->
       error "cannot cast %a to function type"
@@ -6540,7 +6545,8 @@ and mkCastTGen ?(check=true) ?context ?(fromsource=false) ?(force=false)
     end
   else
     let newt = if fromsource then newt else !typeForInsertedCast e oldt newt in
-    if check then checkCast ?context ~fromsource oldt newt;
+    let nullptr_cast = is_nullptr e in
+    if check then checkCast ?context ~nullptr_cast ~fromsource oldt newt;
     (newt, castReduce fromsource force oldt newt e)
 
 and mkCastT ?(check=true) ?(force=false) ~(oldt: typ) ~(newt: typ) e =
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 202240172646694cf72d8211023f7a858620703c..17cda409b1b1f02caf111ddbb60e3e3d0b4915cb 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1020,6 +1020,14 @@ val isConstantOffset: ?is_varinfo_cst:(varinfo -> bool) -> offset -> bool
     constant with value zero *)
 val isZero: exp -> bool
 
+(** True if the given expression is a null pointer, i.e. [0], [(void * )0],
+    which are the two null pointer constants in the standard, or the cast of
+    a null pointer (constant or not) into a pointer type.
+
+    @since Frama-C+dev
+*)
+val is_nullptr: exp -> bool
+
 (** True if the term is the constant 0 *)
 val isLogicZero: term -> bool
 
@@ -1164,16 +1172,20 @@ val need_cast: ?force:bool -> typ -> typ -> bool
     This applies only to implicit casts. Casts already present
     in the source code are exempt from this hook.
 
-    @since Frama-C+dev*)
+    @since Frama-C+dev
+*)
 val typeForInsertedCast: (exp -> typ -> typ -> typ) ref
 
-(** [checkCast context fromsource oldt newt] emits a warning or an error
-    if the cast from [oldt] to [newt] is invalid.
-    Otherwise, doesn't make anything.
-    [fromsource] is [false] (default) if the cast is not from the source.
+(** [checkCast context fromsource nullptr_cast oldt newt] emits a warning
+    or an error if the cast from [oldt] to [newt] is invalid (does nothing
+    otherwise).
+    [nullptr_cast] is [true] iff the expression being casted is a null pointer.
+    Default is false.
+    [fromsource] is [false] (default) if the cast is not present in the source
+    code.
     Check [areCompatibleTypes] documentation for [context].
 
-    Suspicious cases that only emits a warning :
+    Suspicious cases that only emit a warning:
     - Implicit cast from a pointer to an integer.
     - Cast from a pointer to a function type to another pointer to a function
       type when the function types are not compatible.
@@ -1181,21 +1193,24 @@ val typeForInsertedCast: (exp -> typ -> typ -> typ) ref
     - Cast, in both directions, between pointer to an object type and pointer
       to a function type.
 
-    @since Frama-C+dev*)
+    @since Frama-C+dev
+*)
 val checkCast:
-  ?context:qualifier_check_context -> ?fromsource:bool -> typ -> typ -> unit
+  ?context:qualifier_check_context ->
+  ?nullptr_cast:bool ->
+  ?fromsource:bool ->
+  typ -> typ -> unit
 
 
 (** Generic version of {!Cil.mkCastT}.
     Construct a cast when having the old type of the expression.
-    [fromsource] is [false] (default) if the cast is not from the source.
+    [fromsource] is [false] (default) if the cast is not present in the source
+    code.
     If [check] is [true] (default), we check that the cast is valid,
-    fail if the cast is invalid.
+    emitting an error or warning if the cast is invalid.
     If the new type is the same as the old type, then no cast is added,
     unless [force] is [true] (default is [false]).
-    Casting from [oldt] to [newt].
-    Take the expression as argument and can modify it.
-    Return the new type and the new expression.
+    Cast from [oldt] to [newt], returning the new type and the new expression.
 
     @since Frama-C+dev
 *)
@@ -1205,13 +1220,13 @@ val mkCastTGen: ?check:bool -> ?context:qualifier_check_context ->
 (** Construct a cast when having the old type of the expression. If the new
     type is the same as the old type, then no cast is added, unless [force]
     is [true] (default is [false]).
-    Fail if the cast is invalid.
+    Emit an error or warning if [check] is true and the cast is invalid.
     @before 23.0-Vanadium different order of arguments.
     @before Frama-C+dev no [check] argument, it was always [false].
 *)
 val mkCastT: ?check:bool -> ?force:bool -> oldt:typ -> newt:typ -> exp -> exp
 
-(** Like {!Cil.mkCastT} but uses typeOf to get [oldt]
+(** Like {!Cil.mkCastT}, but uses [typeOf] to get [oldt].
     @before 23.0-Vanadium different order of arguments.
     @before Frama-C+dev no [check] argument, it was always [false].
 *)
diff --git a/tests/syntax/nullptr_fct.c b/tests/syntax/nullptr_fct.c
new file mode 100644
index 0000000000000000000000000000000000000000..ca81cf98af7a5e9788b5c1bf85f45b0208160cbc
--- /dev/null
+++ b/tests/syntax/nullptr_fct.c
@@ -0,0 +1,7 @@
+typedef void (*fun)(void);
+
+void wrap (fun f) {
+  if (f != (void*)0) f();
+  if (f != 0) f();
+  if (f != (int*)0) f();
+}
diff --git a/tests/syntax/oracle/nullptr_fct.res.oracle b/tests/syntax/oracle/nullptr_fct.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4df294ff63dff43d77819806823602aca49e4d69
--- /dev/null
+++ b/tests/syntax/oracle/nullptr_fct.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing nullptr_fct.c (with preprocessing)
+/* Generated by Frama-C */
+void wrap(void (*f)(void))
+{
+  if (f != (void (*)(void))0) (*f)();
+  if (f != (void (*)(void))0) (*f)();
+  if (f != (void (*)(void))0) (*f)();
+  return;
+}
+
+