From 2c623d84da92d0549d99936cafbaf04781fdcb63 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 10 Jan 2019 19:36:00 +0100
Subject: [PATCH] [Kernel] be more lenient with function pointer types with
empty argument lists
---
src/kernel_internals/typing/cabs2cil.ml | 8 ++++---
tests/syntax/fct_ptr.i | 4 ++++
tests/syntax/function-types-compatible.i | 2 +-
tests/syntax/oracle/fct_ptr.res.oracle | 14 ++++++++++++
.../function-types-compatible.res.oracle | 22 +++++++++++++++----
5 files changed, 42 insertions(+), 8 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b09617ac5eb..df716861958 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 d6695d92417..6b64b574793 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 48a4e257653..770198b5691 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 af75749caca..5d52398cf87 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 1d6359c914d..121d63a24e7 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;
+}
+
+
--
GitLab