diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index b09617ac5eb3413608e822429cb55b652cb349cb..df7168619585b91a74086ddd6ab9220e1017b4d9 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -2722,9 +2722,11 @@ let rec castTo ?(fromsource=false) | TPtr (TFun (_,args,va,_),_), TPtr(TFun (_,args',va',_),_) -> (* Checks on casting from a function type into another one. We enforce at least the same number of arguments, and emit a warning - if types do not match. - *) - if va <> va' || bigger_length_args args args' then + if types do not match. Note that empty argument lists are always + compatible. *) + if (va <> va' || bigger_length_args args args') && + (args <> None && args' <> None) + then error "conversion between function types with \ different number of arguments:@ %a@ and@ %a" diff --git a/tests/syntax/fct_ptr.i b/tests/syntax/fct_ptr.i index d6695d92417c8112ce3efd5a5ad479b09ca3192b..6b64b57479349ea4bb49e98aba19bcfce06789d3 100644 --- a/tests/syntax/fct_ptr.i +++ b/tests/syntax/fct_ptr.i @@ -14,3 +14,7 @@ int main () { q = p; q(3); } + +typedef int (*Function_ptr)(); +char *f_va(int a, ...) { return a; } +Function_ptr fp_table[1] = {(Function_ptr) f_va}; // warning, but no error diff --git a/tests/syntax/function-types-compatible.i b/tests/syntax/function-types-compatible.i index 48a4e2576539bd7da454db4beda62fbbfabbba9f..770198b5691b45604630bd53effc937be6319407 100644 --- a/tests/syntax/function-types-compatible.i +++ b/tests/syntax/function-types-compatible.i @@ -2,5 +2,5 @@ void (*p)(int, ...); void f(); void main() { p = f; - p(1, 2); + p(1, 2); // warning, but no parsing error; will fail during execution } diff --git a/tests/syntax/oracle/fct_ptr.res.oracle b/tests/syntax/oracle/fct_ptr.res.oracle index af75749caca09e721d7f17a254929cc6370c9ad4..5d52398cf87b25c369598a5169abb0416da348d0 100644 --- a/tests/syntax/oracle/fct_ptr.res.oracle +++ b/tests/syntax/oracle/fct_ptr.res.oracle @@ -1,5 +1,11 @@ [kernel] Parsing tests/syntax/fct_ptr.i (no preprocessing) +[kernel:typing:incompatible-types-call] tests/syntax/fct_ptr.i:20: Warning: + implicit conversion between incompatible function types: + char *(*)(int a , ...) + and + int (*)() /* Generated by Frama-C */ +typedef int (*Function_ptr)(); int f(int); void *p = (void *)(& f); @@ -22,4 +28,12 @@ int main(void) return __retres; } +char *f_va(int a, void * const *__va_params) +{ + char *__retres; + __retres = (char *)a; + return __retres; +} + +Function_ptr fp_table[1] = {(int (*)())(& f_va)}; diff --git a/tests/syntax/oracle/function-types-compatible.res.oracle b/tests/syntax/oracle/function-types-compatible.res.oracle index 1d6359c914d3b90af112d595240fd2c6a8d2396f..121d63a24e7721aba55611f25c673bf25953f32f 100644 --- a/tests/syntax/oracle/function-types-compatible.res.oracle +++ b/tests/syntax/oracle/function-types-compatible.res.oracle @@ -1,8 +1,22 @@ [kernel] Parsing tests/syntax/function-types-compatible.i (no preprocessing) -[kernel] tests/syntax/function-types-compatible.i:4: Failure: - conversion between function types with different number of arguments: +[kernel:typing:incompatible-types-call] tests/syntax/function-types-compatible.i:4: Warning: + implicit conversion between incompatible function types: void (*)() and void (*)(int , ...) -[kernel] User Error: stopping on file "tests/syntax/function-types-compatible.i" that has errors. -[kernel] Frama-C aborted: invalid user input. +/* Generated by Frama-C */ +void (*p)(int , void * const *__va_params); +void f(); + +void main(void) +{ + p = (void (*)(int , void * const *__va_params))(& f); + { + int __va_arg0 = 2; + void *__va_args[1] = {& __va_arg0}; + (*p)(1,(void * const *)(__va_args)); + } + return; +} + +