diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index d292539ff501de4c8b9f12103d3ee0dd60b00f3c..2d2e027c874cbd7b16cac2ccc9beeb35495cadd6 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -6463,7 +6463,7 @@ and doExp local_env *) if not isSpecialBuiltin && not are_ghost then begin warn_no_proto f; - let typ = TFun (resType, Some [], false,attrs) in + let typ = TFun (resType, Some [], false, attrs) in Cil.update_var_type f typ; end | None, _ (* TODO: treat function pointers. *) @@ -6599,6 +6599,17 @@ and doExp local_env (List.mapi default_argument_promotion args) in let typ = TFun (resType, Some prm_types, false,attrs) in + begin + try + (* Nested calls of a function without a prototype : inner + calls will update f type but the information is not + communicated to outer ones, hence [argTypes] is not up to + date and we need to check that types are compagtibles. *) + ignore(Cil.compatibleTypes f.vtype typ); + with Cannot_combine msg -> + abort_context "nested calls of %s without a prototype and \ + incompatible arguments : %s" f.vname msg + end; Cil.update_var_type f typ; Cil.setFormalsDecl f typ; (chunk,args) diff --git a/tests/syntax/implicit-calls.c b/tests/syntax/implicit-calls.c new file mode 100644 index 0000000000000000000000000000000000000000..0fdff0fcf9374d5c40a342d752a49799846fdbd3 --- /dev/null +++ b/tests/syntax/implicit-calls.c @@ -0,0 +1,13 @@ +/* run.config + EXIT: 1 + STDOPT: #"-cpp-extra-args=-DINCOMP1" + STDOPT: #"-cpp-extra-args=-DINCOMP2" +*/ + +#ifdef INCOMP1 + void foo(unsigned x) { bar(bar(0, 12), x); } +#endif + +#ifdef INCOMP2 + void foo(int x) { bar(bar(0), x); } +#endif diff --git a/tests/syntax/oracle/implicit-calls.0.res.oracle b/tests/syntax/oracle/implicit-calls.0.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..f562290d907587dca20667ebf350d307b98293c7 --- /dev/null +++ b/tests/syntax/oracle/implicit-calls.0.res.oracle @@ -0,0 +1,13 @@ +[kernel] Parsing implicit-calls.c (with preprocessing) +[kernel:typing:implicit-function-declaration] implicit-calls.c:8: Warning: + Calling undeclared function bar. Old style K&R code? +[kernel] implicit-calls.c:8: User Error: + nested calls of bar without a prototype and incompatible arguments : different integer types: + 'int' and 'unsigned int' + 6 + 7 #ifdef INCOMP1 + 8 void foo(unsigned x) { bar(bar(0, 12), x); } + ^^^^^^^^^^^^^^^^^^ + 9 #endif + 10 +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/implicit-calls.1.res.oracle b/tests/syntax/oracle/implicit-calls.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..1a6e4fe87915ce013a6a947a16814b61784f37c9 --- /dev/null +++ b/tests/syntax/oracle/implicit-calls.1.res.oracle @@ -0,0 +1,11 @@ +[kernel] Parsing implicit-calls.c (with preprocessing) +[kernel:typing:implicit-function-declaration] implicit-calls.c:12: Warning: + Calling undeclared function bar. Old style K&R code? +[kernel] implicit-calls.c:12: User Error: + nested calls of bar without a prototype and incompatible arguments : different number of arguments + 10 + 11 #ifdef INCOMP2 + 12 void foo(int x) { bar(bar(0), x); } + ^^^^^^^^^^^^^^ + 13 #endif +[kernel] Frama-C aborted: invalid user input.