From b666f1a05393f83a61db4e575d784bd3859b55a4 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 25 Sep 2023 17:02:42 +0200
Subject: [PATCH] [kernel] fix missing function designator conversions to
function ptr.
... but do not convert too many either.
---
src/kernel_internals/typing/cabs2cil.ml | 5 +++--
tests/syntax/nullptr_fct.c | 4 ++++
tests/syntax/oracle/nullptr_fct.res.oracle | 1 +
3 files changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 5d267f9428f..01377897fd6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5328,7 +5328,6 @@ and doExp local_env
match e.enode, unrollType t with
| (Lval(lv) | CastE(_, {enode = Lval lv})), TArray(tbase, _, a) ->
mkStartOfAndMark loc lv, TPtr(tbase, a)
- | Lval(Mem _, _), TFun _ -> e, t (* Do not turn pointer function types *)
| (Lval(lv) | CastE(_, {enode = Lval lv})), TFun _ ->
mkAddrOfAndMark loc lv, TPtr(t, [])
| _, (TArray _ | TFun _) ->
@@ -6016,7 +6015,9 @@ and doExp local_env
if asconst = CConst then
Kernel.warning ~current:true "ASSIGN in constant";
let se0 = unspecified_chunk empty in
- let (r1,se1, e1', lvt) = doExp local_env CNoConst e (AExp None) in
+ let (r1,se1, e1', lvt) =
+ doExp local_env CNoConst e AExpLeaveArrayFun
+ in
let lv =
match e1'.enode with
| Lval x when Cil.is_modifiable_lval x -> x
diff --git a/tests/syntax/nullptr_fct.c b/tests/syntax/nullptr_fct.c
index ca81cf98af7..8c61df5c2ec 100644
--- a/tests/syntax/nullptr_fct.c
+++ b/tests/syntax/nullptr_fct.c
@@ -4,4 +4,8 @@ void wrap (fun f) {
if (f != (void*)0) f();
if (f != 0) f();
if (f != (int*)0) f();
+ /* must also work when there's an implicit conversion from function
+ designator to function type...
+ */
+ if (*f != 0) (*f)();
}
diff --git a/tests/syntax/oracle/nullptr_fct.res.oracle b/tests/syntax/oracle/nullptr_fct.res.oracle
index 4df294ff63d..c2c534d51fa 100644
--- a/tests/syntax/oracle/nullptr_fct.res.oracle
+++ b/tests/syntax/oracle/nullptr_fct.res.oracle
@@ -5,6 +5,7 @@ void wrap(void (*f)(void))
if (f != (void (*)(void))0) (*f)();
if (f != (void (*)(void))0) (*f)();
if (f != (void (*)(void))0) (*f)();
+ if (f != (void (*)(void))0) (*f)();
return;
}
--
GitLab