diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 5d267f9428f6d0848eb021cdf293489b2a87ffd9..01377897fd649ccc3e36047fd7d44f1ade39b86d 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 ca81cf98af7a5e9788b5c1bf85f45b0208160cbc..8c61df5c2ec5a44cd338d6c93efc7bb596a16968 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 4df294ff63dff43d77819806823602aca49e4d69..c2c534d51faf32733af162c45951c8287954a13e 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; }