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..fbe73e72e7bf26d24cdedecda4f746e0a7fc88f9 100644
--- a/tests/syntax/const-assignments.c
+++ b/tests/syntax/const-assignments.c
@@ -12,6 +12,7 @@
STDOPT: +" -cpp-extra-args=-DT7"
EXIT:1
STDOPT: +" -cpp-extra-args=-DT8"
+ STDOPT: +" -cpp-extra-args=-DT9" +"-kernel-warn-key typing:incompatible-types-call=abort"
*/
/* The first run is correct. The others should fail, as they include invalid
assignments to const lvalues. */
@@ -73,9 +74,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 +93,24 @@ 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);
+#ifdef T9
+ /* KO: although s has the __fc_initialized_object attribute, z[0] has not (and
+ cannot) and y is const. */
+ k2(&s->z[0]->y);
+#endif
+}
+
#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..de3d0783c7c8bdccc47d733735a199338ff9816e 100644
--- a/tests/syntax/oracle/const-assignments.0.res.oracle
+++ b/tests/syntax/oracle/const-assignments.0.res.oracle
@@ -1,10 +1,11 @@
[kernel] Parsing const-assignments.c (with preprocessing)
/* 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 +32,18 @@ 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));
+ return;
+}
+
diff --git a/tests/syntax/oracle/const-assignments.1.res.oracle b/tests/syntax/oracle/const-assignments.1.res.oracle
index 195e9432c3555aca11aa92de91a32b05d21cf62e..038ab482208c4f531c62dc10d5e6c86f1d9c1e49 100644
--- a/tests/syntax/oracle/const-assignments.1.res.oracle
+++ b/tests/syntax/oracle/const-assignments.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:21: User Error:
+[kernel] const-assignments.c:22: User Error:
Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.10.res.oracle b/tests/syntax/oracle/const-assignments.10.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..aaee700de3e0333d391e2524439b518ab3b5d152
--- /dev/null
+++ b/tests/syntax/oracle/const-assignments.10.res.oracle
@@ -0,0 +1,7 @@
+[kernel] Parsing const-assignments.c (with preprocessing)
+[kernel:typing:incompatible-types-call] const-assignments.c:110: Warning:
+ expected 'int *' but got argument of type 'int const *': & (s->z[0])->y
+[kernel] User Error: warning typing:incompatible-types-call treated as fatal error.
+[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/const-assignments.2.res.oracle b/tests/syntax/oracle/const-assignments.2.res.oracle
index e253406148ecb9fe1f8e77d7a0fb8e4bd88414a6..67303a701fca626253759917c6a8d7ef31be47fa 100644
--- a/tests/syntax/oracle/const-assignments.2.res.oracle
+++ b/tests/syntax/oracle/const-assignments.2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:27: User Error:
+[kernel] const-assignments.c:28: User Error:
Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.3.res.oracle b/tests/syntax/oracle/const-assignments.3.res.oracle
index 33c4bad33a33015d727a3c3a3f5dae7fbca66b67..79768f7799b608b775963b5a3463710cdcb47635 100644
--- a/tests/syntax/oracle/const-assignments.3.res.oracle
+++ b/tests/syntax/oracle/const-assignments.3.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:33: User Error:
+[kernel] const-assignments.c:34: User Error:
Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.4.res.oracle b/tests/syntax/oracle/const-assignments.4.res.oracle
index 8c9c93e9c82c5e04902d4a665fb2d152e612fcb8..0ae872708907a5410141a74efc231c127126d7e8 100644
--- a/tests/syntax/oracle/const-assignments.4.res.oracle
+++ b/tests/syntax/oracle/const-assignments.4.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:39: User Error:
+[kernel] const-assignments.c:40: User Error:
Cannot assign to non-modifiable lval x
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.5.res.oracle b/tests/syntax/oracle/const-assignments.5.res.oracle
index b7aa22f538e9eae22eea1cab7b0bfc7fa9dfe983..395f59284a48ac86eca556a12c95f23a5078c816 100644
--- a/tests/syntax/oracle/const-assignments.5.res.oracle
+++ b/tests/syntax/oracle/const-assignments.5.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:46: User Error:
+[kernel] const-assignments.c:47: User Error:
Cannot assign to non-modifiable lval x_0
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.6.res.oracle b/tests/syntax/oracle/const-assignments.6.res.oracle
index f05bcf02955448caf41e171a2b5bc9a506be37ae..349d3259223c8124771466cdf8c806797e50d91a 100644
--- a/tests/syntax/oracle/const-assignments.6.res.oracle
+++ b/tests/syntax/oracle/const-assignments.6.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:52: User Error:
+[kernel] const-assignments.c:53: User Error:
Cannot assign to non-modifiable lval *x_0
[kernel] User Error: stopping on file "const-assignments.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
diff --git a/tests/syntax/oracle/const-assignments.7.res.oracle b/tests/syntax/oracle/const-assignments.7.res.oracle
index 91a4f1b2285c3d704a1ce62f7d2864b47e0927e2..f397d365bcaad40d3e5369fe61c74f07918b368c 100644
--- a/tests/syntax/oracle/const-assignments.7.res.oracle
+++ b/tests/syntax/oracle/const-assignments.7.res.oracle
@@ -1,12 +1,13 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel:typing:incompatible-types-call] const-assignments.c:60: Warning:
+[kernel:typing:incompatible-types-call] const-assignments.c:61: Warning:
expected 'int *' but got argument of type 'int const *': & x
/* 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 +40,18 @@ 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));
+ return;
+}
+
diff --git a/tests/syntax/oracle/const-assignments.8.res.oracle b/tests/syntax/oracle/const-assignments.8.res.oracle
index 97f911954ffc5ad8cc2e7b391476dc4b18b7bee4..281cae543fca4f7190a43e578eced91b459f2ba8 100644
--- a/tests/syntax/oracle/const-assignments.8.res.oracle
+++ b/tests/syntax/oracle/const-assignments.8.res.oracle
@@ -1,12 +1,13 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel:typing:incompatible-types-call] const-assignments.c:66: Warning:
+[kernel:typing:incompatible-types-call] const-assignments.c:67: Warning:
expected 'int *' but got argument of type 'int const *': x_0
/* 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 +40,18 @@ 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));
+ return;
+}
+
diff --git a/tests/syntax/oracle/const-assignments.9.res.oracle b/tests/syntax/oracle/const-assignments.9.res.oracle
index ae9db5d4373f3e76db067f41226076ea2b63c4ff..7d532fb832d1b38c4f5eba24de67bdaf9429055c 100644
--- a/tests/syntax/oracle/const-assignments.9.res.oracle
+++ b/tests/syntax/oracle/const-assignments.9.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing const-assignments.c (with preprocessing)
-[kernel] const-assignments.c:101: User Error:
+[kernel] const-assignments.c:121: 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.