diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f3b479e9c0745c243ba404dee8ce6e8acd4e4c8b..506bf706f271405e21544102503885ce36a9dff6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2704,51 +2704,92 @@ let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ =
let get_qualifiers t = Cil.filter_qualifier_attributes (Cil.typeAttrs t)
-let equal_qualifiers a1 a2 =
- Cil_datatype.Attributes.equal
- (Cil.filter_qualifier_attributes a1) (Cil.filter_qualifier_attributes a2)
+(* how type qualifiers must be checked *)
+type qualifier_check_context =
+ | Identical (* identical qualifiers. *)
+ | IdenticalToplevel (* ignore at toplevel, use Identical when going under a
+ pointer. *)
+ | Covariant (* first type can have const-qualifications
+ the second doesn't have. *)
+ | CovariantToplevel
+ (* accepts everything for current type, use Covariant when going under a
+ pointer. *)
+ | Contravariant (* second type can have const-qualifications
+ the first doesn't have. *)
+ | ContravariantToplevel
+ (* accepts everything for current type, use Contravariant when going under
+ a pointer. *)
+
+let qualifier_context_fun_arg = function
+ | Identical | IdenticalToplevel -> IdenticalToplevel
+ | Covariant | CovariantToplevel -> ContravariantToplevel
+ | Contravariant | ContravariantToplevel -> CovariantToplevel
+
+let qualifier_context_fun_ret = function
+ | Identical | IdenticalToplevel -> IdenticalToplevel
+ | Covariant | CovariantToplevel -> CovariantToplevel
+ | Contravariant | ContravariantToplevel -> ContravariantToplevel
+
+let qualifier_context_ptr = function
+ | Identical | IdenticalToplevel -> Identical
+ | Covariant | CovariantToplevel -> Covariant
+ | Contravariant | ContravariantToplevel -> Contravariant
+
+let included_qualifiers ?(context=Identical) a1 a2 =
+ let a1 = Cil.filter_qualifier_attributes a1 in
+ let a2 = Cil.filter_qualifier_attributes a2 in
+ let a1 = Cil.dropAttribute "restrict" a1 in
+ let a2 = Cil.dropAttribute "restrict" a2 in
+ let a1_no_const = Cil.dropAttribute "const" a1 in
+ let a2_no_const = Cil.dropAttribute "const" a2 in
+ let is_equal = Cil_datatype.Attributes.equal a1 a2 in
+ if is_equal then true
+ else begin
+ match context with
+ | Identical -> false
+ | Covariant -> Cil_datatype.Attributes.equal a1_no_const a2
+ | Contravariant -> Cil_datatype.Attributes.equal a1 a2_no_const
+ | CovariantToplevel | ContravariantToplevel | IdenticalToplevel -> true
+ end
(* precondition: t1 and t2 must be "compatible" as per combineTypes, i.e.
- you must have called [combineTypes t1 t2] before calling this function.
- When [relaxed] is true, qualifier differences are ignored; this is
- an internal parameter used during recursive calls.
- The qualifier compatibility algorithm is:
- - by default, type qualifiers are ignored (e.g. for basic types);
- - when entering a pointer type, stop ignoring type qualifiers;
- - when entering a function type, resume ignoring type qualifiers. *)
-let rec have_compatible_qualifiers_deep ?(relaxed=false) t1 t2 =
+ you must have called [combineTypes t1 t2] before calling this function. *)
+let rec have_compatible_qualifiers_deep ?(context=Identical) t1 t2 =
match unrollType t1, unrollType t2 with
| TFun (tres1, Some args1, _, _), TFun (tres2, Some args2, _, _) ->
- have_compatible_qualifiers_deep ~relaxed:true tres1 tres2 &&
+ have_compatible_qualifiers_deep
+ ~context:(qualifier_context_fun_ret context) tres1 tres2 &&
+ let context = qualifier_context_fun_arg context in
List.for_all2 (fun (_, t1', a1) (_, t2', a2) ->
- have_compatible_qualifiers_deep ~relaxed:true t1' t2' &&
- equal_qualifiers a1 a2)
+ have_compatible_qualifiers_deep ~context t1' t2' &&
+ included_qualifiers ~context a1 a2)
args1 args2
| TPtr (t1', a1), TPtr (t2', a2)
| TArray (t1', _, _, a1), TArray (t2', _, _, a2) ->
- have_compatible_qualifiers_deep ~relaxed:false t1' t2' &&
- (relaxed || equal_qualifiers a1 a2)
- | _, _ -> relaxed || equal_qualifiers (Cil.typeAttrs t1) (Cil.typeAttrs t2)
+ (included_qualifiers ~context a1 a2) &&
+ let context = qualifier_context_ptr context in
+ have_compatible_qualifiers_deep ~context t1' t2'
+ | _, _ -> included_qualifiers ~context (Cil.typeAttrs t1) (Cil.typeAttrs t2)
-let compatibleTypes t1 t2 =
+let compatibleTypes ?context t1 t2 =
try
let r = combineTypes CombineOther t1 t2 in
(* C99, 6.7.3 §9: "... to be compatible, both shall have the identically
qualified version of a compatible type;" *)
- if not (have_compatible_qualifiers_deep t1 t2) then
+ if not (have_compatible_qualifiers_deep ?context t1 t2) then
raise (Cannot_combine "different qualifiers");
(* Note: different non-qualifier attributes will be silently dropped. *)
r
with Cannot_combine _ as e ->
raise e
-let areCompatibleTypes t1 t2 =
+let areCompatibleTypes ?context t1 t2 =
try
- ignore (compatibleTypes t1 t2); true
+ ignore (compatibleTypes ?context t1 t2); true
with Cannot_combine _ -> false
(* Specify whether the cast is from the source code *)
-let rec castTo ?(fromsource=false)
+let rec castTo ?context ?(fromsource=false)
(ot : typ) (nt : typ) (e : exp) : (typ * exp ) =
Kernel.debug ~dkey:Kernel.dkey_typing_cast "@[%t: castTo:%s %a->%a@\n@]"
Cil.pp_thisloc (if fromsource then "(source)" else "")
@@ -2803,7 +2844,7 @@ let rec castTo ?(fromsource=false)
"conversion between function types with \
different number of arguments:@ %a@ and@ %a"
Cil_printer.pp_typ ot Cil_printer.pp_typ nt;
- if not (areCompatibleTypes ot nt) then
+ if not (areCompatibleTypes ?context ot nt) then
Kernel.warning
~wkey:Kernel.wkey_incompatible_types_call
~current:true
@@ -2818,7 +2859,7 @@ let rec castTo ?(fromsource=false)
| Lval lv -> Cil.mkAddrOf ~loc:e.eloc lv
| _ -> e (* function decay into pointer anyway *)
in
- castTo ~fromsource (TPtr (ot', [])) nt' clean_e
+ castTo ?context ~fromsource (TPtr (ot', [])) nt' clean_e
(* accept converting a ptr to function to/from a ptr to void, even though
not really accepted by the standard. gcc supports it. though
@@ -2834,10 +2875,10 @@ let rec castTo ?(fromsource=false)
original type in the sources.
*)
| TPtr(TFun _,_), TPtr(TNamed(ti,nattr),pattr) ->
- castTo
+ castTo ?context
~fromsource ot (TPtr (Cil.typeAddAttributes nattr ti.ttype, pattr)) e
| TPtr(TNamed(ti,nattr),pattr), TPtr(TFun _,_) ->
- castTo
+ castTo ?context
~fromsource (TPtr (Cil.typeAddAttributes nattr ti.ttype, pattr)) nt e
(* No other conversion implying a pointer to function
@@ -2938,7 +2979,7 @@ let rec castTo ?(fromsource=false)
Cil_printer.pp_exp e
in
(* Continue casting *)
- castTo ~fromsource:fromsource fstfield.ftype nt' e'
+ castTo ?context ~fromsource:fromsource fstfield.ftype nt' e'
end
end
| _ ->
@@ -6603,7 +6644,9 @@ and doExp local_env
in
(add_reads ~ghost:local_env.is_ghost loc r c, e, t)
in
- let (texpected, a'') = castTo att at a' in
+ let (texpected, a'') =
+ castTo ~context:ContravariantToplevel att at a'
+ in
(* A posteriori check that the argument type was compatible,
to generate a warning otherwise;
if a'' = a', no check needs to be done (no cast was introduced).
@@ -6631,11 +6674,7 @@ and doExp local_env
(Cil.isAnyCharPtrType texpected && Cil.isVoidPtrType att) ||
(* always allow null pointers *)
(Cil.isPointerType texpected && Ast_info.is_null_expr a') ||
- areCompatibleTypes texpected att ||
- (let texpected_no_qualif =
- Cil.typeRemoveAttributesDeep ["const"; "restrict"] texpected
- in
- areCompatibleTypes texpected_no_qualif att)
+ areCompatibleTypes ~context:ContravariantToplevel att texpected
in
let ok =
if ok1 then true
@@ -10220,6 +10259,9 @@ let convFile (path, f) =
globinitcalled = false;
}
+(* export function without internal `relaxed' argument. *)
+let areCompatibleTypes t1 t2 = areCompatibleTypes t1 t2
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/tests/syntax/const_formals.i b/tests/syntax/const_formals.i
new file mode 100644
index 0000000000000000000000000000000000000000..ceba7f1c8ce2e5a0aea490d867a17bacaae1f22a
--- /dev/null
+++ b/tests/syntax/const_formals.i
@@ -0,0 +1,34 @@
+const char* s = "foo";
+char mutable_s[] = "bar";
+const char**p = &s;
+
+char f(const char* s) { return s[0]; }
+
+char g(const char* const* a) { return **a; }
+
+// we ignore restrict differences. GCC and Clang do that too
+void foo(int *restrict x, int* y);
+void foo(int *x, int* restrict y) { *x++; *y--; }
+
+// play a little bit with function pointers.
+int incr_get(int* x) { *x++; return *x; }
+
+int get(const int*x) { return *x; }
+
+int apply_const(int* x, int (*g)(const int*y)) {
+ return g(x);
+}
+
+int apply_non_const (int* x, int(*g)(int*y)) {
+ return g(x);
+}
+
+int main() {
+ int x = 1;
+ apply_const(&x,incr_get); // should warn
+ apply_non_const(&x,incr_get); // ok
+ apply_const(&x,get); // ok
+ apply_non_const(&x,get); // ok
+ char c = f(mutable_s); // implicit conversion should not raise warning
+ char d = g(p); // implicit conversion should not raise warning
+}
diff --git a/tests/syntax/oracle/const_formals.res.oracle b/tests/syntax/oracle/const_formals.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b3375fd904feb5b2d08097ab2785ec2cfda54cb3
--- /dev/null
+++ b/tests/syntax/oracle/const_formals.res.oracle
@@ -0,0 +1,88 @@
+[kernel] Parsing tests/syntax/const_formals.i (no preprocessing)
+[kernel:typing:incompatible-types-call] tests/syntax/const_formals.i:28: Warning:
+ implicit conversion between incompatible function types:
+ int (*)(int *x)
+ and
+ int (*)(int const *y)
+[kernel:typing:incompatible-types-call] tests/syntax/const_formals.i:28: Warning:
+ expected 'int (*)(int const *y)' but got argument of type 'int (*)(int *x)': & incr_get
+/* Generated by Frama-C */
+char const *s = "foo";
+char mutable_s[4] = {(char)'b', (char)'a', (char)'r', (char)'\000'};
+char const **p = & s;
+char f(char const *s_0)
+{
+ char __retres;
+ __retres = *(s_0 + 0);
+ return __retres;
+}
+
+char g(char const * const *a)
+{
+ char __retres;
+ __retres = *(*a);
+ return __retres;
+}
+
+void foo(int *x, int * __restrict y);
+
+void foo(int *x, int * __restrict y)
+{
+ int *tmp;
+ int *tmp_0;
+ tmp = x;
+ x ++;
+ ;
+ tmp_0 = y;
+ y --;
+ ;
+ return;
+}
+
+int incr_get(int *x)
+{
+ int __retres;
+ int *tmp;
+ tmp = x;
+ x ++;
+ ;
+ __retres = *x;
+ return __retres;
+}
+
+int get(int const *x)
+{
+ int __retres;
+ __retres = *x;
+ return __retres;
+}
+
+int apply_const(int *x, int (*g_0)(int const *y))
+{
+ int tmp;
+ tmp = (*g_0)((int const *)x);
+ return tmp;
+}
+
+int apply_non_const(int *x, int (*g_0)(int *y))
+{
+ int tmp;
+ tmp = (*g_0)(x);
+ return tmp;
+}
+
+int main(void)
+{
+ int __retres;
+ int x = 1;
+ apply_const(& x,(int (*)(int const *y))(& incr_get));
+ apply_non_const(& x,& incr_get);
+ apply_const(& x,& get);
+ apply_non_const(& x,(int (*)(int *y))(& get));
+ char c = f((char const *)(mutable_s));
+ char d = g((char const * const *)p);
+ __retres = 0;
+ return __retres;
+}
+
+