diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 13006c859426f3ebde563fd698077ba99ec641b1..33c490766639008f250eaf67a617a3cdb5b4c532 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6877,8 +6877,17 @@ and doExp local_env
(Cil.isPointerType texpected && Ast_info.is_null_expr a') ||
areCompatibleTypes ~context:ContravariantToplevel att texpected
in
+ let ok2 =
+ (* accept pointer to const type as long as the respective
+ argument (formal) is annotated with __fc_initialized_object
+ attribute. *)
+ let arg_is_initialized = Cil.is_initialized a' in
+ arg_is_initialized
+ && Cil.isPointerType texpected
+ && areCompatibleTypes ~context:CovariantToplevel att texpected
+ in
let ok =
- if ok1 then true
+ if ok1 || ok2 then true
(* special warning for void* -> any* conversions;
this is equivalent to option '-Wc++-compat' in GCC *)
else if Cil.isVoidPtrType att && Cil.isPointerType texpected
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 0ca631c1f05375f17c32143745b609033e28194f..82e08770fa7d4e69435957afd2621665c4fdb9eb 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6239,23 +6239,38 @@ and is_complete_agg_member ~allowZeroSizeArrays ?last_field t =
let isCompleteType ?allowZeroSizeArrays t =
isCompleteType ?allowZeroSizeArrays t
-let is_mutable_or_initialized (host, offset) =
+let is_mutable (lhost, offset) =
let rec aux can_mutate typ off =
let can_mutate = can_mutate && not (isConstType typ) in
match unrollType typ, off with
| _, NoOffset -> can_mutate
| _, Field (fi, off) ->
- aux
- (can_mutate || hasAttribute frama_c_mutable fi.fattr)
- fi.ftype off
+ let can_mutate = can_mutate || hasAttribute frama_c_mutable fi.fattr in
+ aux can_mutate fi.ftype off
| TArray(typ, _, _), Index(_, off) -> aux can_mutate typ off
- | _, Index _ -> Kernel.fatal "Index on a non-array type"
+ | typ, Index _ ->
+ Kernel.fatal "Index on a non-array type '%a'" Cil_datatype.Typ.pretty typ
in
- match host with
- | Mem({ enode = Lval (Var vi, NoOffset) })
- when hasAttribute frama_c_init_obj vi.vattr -> true
- | _ ->
- aux false (typeOfLhost host) offset
+ aux false (typeOfLhost lhost) offset
+
+let rec is_initialized_aux on_same_obj e =
+ match e.enode with
+ | Lval (lh, _) | AddrOf (lh, _) | StartOf (lh, _) ->
+ is_initialized_lhost on_same_obj lh
+ | BinOp ((PlusPI|MinusPI), e, _, _) | CastE (_, e) ->
+ is_initialized_aux on_same_obj e
+ | _ -> false
+
+and is_initialized_lhost on_same_obj lhost =
+ match lhost with
+ | Var vi -> hasAttribute frama_c_init_obj vi.vattr
+ | Mem e -> on_same_obj && is_initialized_aux false e
+
+let is_initialized e =
+ is_initialized_aux true e
+
+let is_mutable_or_initialized lval =
+ is_mutable lval || is_initialized_lhost true (fst lval)
let is_modifiable_lval lv =
let t = typeOfLval lv in
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 005bc7a063469332ff0ab80f24dbf8ad3778d501..9a2b27a1f4f4807ef7b5ef4e4267d172e8fbfdac 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1254,6 +1254,10 @@ val frama_c_mutable: string
*)
val frama_c_inlined: string
+(** [true] if the underlying left-value of the given expression is allowed to be
+ assigned to thanks to a [frama_c_init_obj] attribute. *)
+val is_initialized: exp -> bool
+
(** [true] if the given lval is allowed to be assigned to thanks to
a [frama_c_init_obj] or a [frama_c_mutable] attribute.
*)
diff --git a/tests/syntax/const-assignments.c b/tests/syntax/const-assignments.c
index 745a67aa56aac5491708a37f4d6e282f1f5c2723..caa00564dc0548a83057048cafe084a1d51d0e8e 100644
--- a/tests/syntax/const-assignments.c
+++ b/tests/syntax/const-assignments.c
@@ -73,9 +73,10 @@ void h(const int* x) {
g(y);
}
-typedef struct {
+typedef struct S {
__attribute__((__fc_mutable)) int x;
const int y;
+ struct S* z[3];
} S;
void build_S(
@@ -91,6 +92,22 @@ void mutable_test(const S* s) {
s->x += 2;
}
+extern void k1(S*);
+extern void k2(int*);
+
+void mutable_test_call(__attribute__((__fc_initialized_object)) const S* s) {
+ /* Although these calls would make losing the const qualifier, this is OK due
+ to the __fc_initialized_object attribute on s. */
+ k1(s);
+ k1(s->z[0]);
+ int a = 1;
+ k1(a + (s + 2));
+ k2(&(s + 2)->y);
+ /* KO: although s has the __fc_initialized_object attribute, z[0] has not (and
+ cannot) and y is const. */
+ k2(&s->z[0]->y);
+}
+
#ifdef T8
typedef struct {
diff --git a/tests/syntax/oracle/const-assignments.0.res.oracle b/tests/syntax/oracle/const-assignments.0.res.oracle
index 2e6713963fde6d1becddee17c529d2fc43b8a7aa..8e1f025840a55596efdf118439d9065a193710a9 100644
--- a/tests/syntax/oracle/const-assignments.0.res.oracle
+++ b/tests/syntax/oracle/const-assignments.0.res.oracle
@@ -1,10 +1,13 @@
[kernel] Parsing const-assignments.c (with preprocessing)
+[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
/* Generated by Frama-C */
-struct __anonstruct_S_1 {
+struct S {
int x ;
int const y ;
+ struct S *z[3] ;
};
-typedef struct __anonstruct_S_1 S;
+typedef struct S S;
int const x = 1;
extern void g(int *p);
@@ -31,4 +34,19 @@ void mutable_test(S const *s)
return;
}
+extern void k1(S *);
+
+extern void k2(int *);
+
+void mutable_test_call(S const *s)
+{
+ k1((S *)s);
+ k1(s->z[0]);
+ int a = 1;
+ k1((S *)((s + 2) + a));
+ k2((int *)(& (s + 2)->y));
+ k2((int *)(& (s->z[0])->y));
+ return;
+}
+
diff --git a/tests/syntax/oracle/const-assignments.7.res.oracle b/tests/syntax/oracle/const-assignments.7.res.oracle
index 91a4f1b2285c3d704a1ce62f7d2864b47e0927e2..28fb4fda51942323ab613869ae6b9fff453bbeee 100644
--- a/tests/syntax/oracle/const-assignments.7.res.oracle
+++ b/tests/syntax/oracle/const-assignments.7.res.oracle
@@ -1,12 +1,15 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel:typing:incompatible-types-call] const-assignments.c:60: Warning:
expected 'int *' but got argument of type 'int const *': & x
+[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
/* Generated by Frama-C */
-struct __anonstruct_S_1 {
+struct S {
int x ;
int const y ;
+ struct S *z[3] ;
};
-typedef struct __anonstruct_S_1 S;
+typedef struct S S;
int const x = 1;
extern void g(int *p);
@@ -39,4 +42,19 @@ void mutable_test(S const *s)
return;
}
+extern void k1(S *);
+
+extern void k2(int *);
+
+void mutable_test_call(S const *s)
+{
+ k1((S *)s);
+ k1(s->z[0]);
+ int a = 1;
+ k1((S *)((s + 2) + a));
+ k2((int *)(& (s + 2)->y));
+ k2((int *)(& (s->z[0])->y));
+ return;
+}
+
diff --git a/tests/syntax/oracle/const-assignments.8.res.oracle b/tests/syntax/oracle/const-assignments.8.res.oracle
index 97f911954ffc5ad8cc2e7b391476dc4b18b7bee4..ee37293dbcb604246197f3309fd0e31ace6a5be5 100644
--- a/tests/syntax/oracle/const-assignments.8.res.oracle
+++ b/tests/syntax/oracle/const-assignments.8.res.oracle
@@ -1,12 +1,15 @@
[kernel] Parsing const-assignments.c (with preprocessing)
[kernel:typing:incompatible-types-call] const-assignments.c:66: Warning:
expected 'int *' but got argument of type 'int const *': x_0
+[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
/* Generated by Frama-C */
-struct __anonstruct_S_1 {
+struct S {
int x ;
int const y ;
+ struct S *z[3] ;
};
-typedef struct __anonstruct_S_1 S;
+typedef struct S S;
int const x = 1;
extern void g(int *p);
@@ -39,4 +42,19 @@ void mutable_test(S const *s)
return;
}
+extern void k1(S *);
+
+extern void k2(int *);
+
+void mutable_test_call(S const *s)
+{
+ k1((S *)s);
+ k1(s->z[0]);
+ int a = 1;
+ k1((S *)((s + 2) + a));
+ k2((int *)(& (s + 2)->y));
+ k2((int *)(& (s->z[0])->y));
+ return;
+}
+
diff --git a/tests/syntax/oracle/const-assignments.9.res.oracle b/tests/syntax/oracle/const-assignments.9.res.oracle
index ae9db5d4373f3e76db067f41226076ea2b63c4ff..ec0fc31a9236c7dba702341a780aba577ec3237d 100644
--- a/tests/syntax/oracle/const-assignments.9.res.oracle
+++ b/tests/syntax/oracle/const-assignments.9.res.oracle
@@ -1,5 +1,7 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:101: User Error:
+[kernel:typing:incompatible-types-call] const-assignments.c:108: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
+[kernel] const-assignments.c:118: User Error:
Cannot assign to non-modifiable lval t->s.y
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.