From 422936919e8a50a4883ecd1fa1ca04e3854ef03d Mon Sep 17 00:00:00 2001
From: tibo <thi.martin.pro@pm.me>
Date: Tue, 16 Apr 2024 16:27:37 +0200
Subject: [PATCH] [cabs2cil] Check argument compatibility for calls without a
prototype
---
src/kernel_internals/typing/cabs2cil.ml | 13 ++++++++++++-
tests/syntax/implicit-calls.c | 13 +++++++++++++
tests/syntax/oracle/implicit-calls.0.res.oracle | 13 +++++++++++++
tests/syntax/oracle/implicit-calls.1.res.oracle | 11 +++++++++++
4 files changed, 49 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/implicit-calls.c
create mode 100644 tests/syntax/oracle/implicit-calls.0.res.oracle
create mode 100644 tests/syntax/oracle/implicit-calls.1.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index d292539ff50..2d2e027c874 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 00000000000..0fdff0fcf93
--- /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 00000000000..f562290d907
--- /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 00000000000..1a6e4fe8791
--- /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.
--
GitLab