From d015e24476448406e88e825d1439b03d514a9460 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 21 Sep 2023 19:37:29 +0200
Subject: [PATCH] [kernel] do not warn on null pointer conversions, even to
function pointer
---
src/kernel_services/ast_queries/cil.ml | 34 +++++++++++++---------
src/kernel_services/ast_queries/cil.mli | 19 ++++++++++--
tests/syntax/nullptr_fct.c | 7 +++++
tests/syntax/oracle/nullptr_fct.res.oracle | 11 +++++++
4 files changed, 54 insertions(+), 17 deletions(-)
create mode 100644 tests/syntax/nullptr_fct.c
create mode 100644 tests/syntax/oracle/nullptr_fct.res.oracle
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 94be68f46f2..ae7aef2e3c2 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 20224017264..41a637c77a3 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 norm, 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
@@ -1167,9 +1175,11 @@ val need_cast: ?force:bool -> typ -> typ -> bool
@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.
+(** [checkCast context fromsource nullptr_cast oldt newt] emits a warning
+ or an error if the cast from [oldt] to [newt] is invalid.
Otherwise, doesn't make anything.
+ [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 from the source.
Check [areCompatibleTypes] documentation for [context].
@@ -1183,7 +1193,10 @@ val typeForInsertedCast: (exp -> typ -> typ -> typ) ref
@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}.
diff --git a/tests/syntax/nullptr_fct.c b/tests/syntax/nullptr_fct.c
new file mode 100644
index 00000000000..ca81cf98af7
--- /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 00000000000..4df294ff63d
--- /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;
+}
+
+
--
GitLab