diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 57941a646de326fbc9d37325cd9bb78c095c69aa..6a38cc02b3662b0a9b5381992257f57b284e3153 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6330,13 +6330,10 @@ let areCompatibleTypes ?strictReturnTypes ?context t1 t2 =
(******************** CASTING *****)
let checkCast ?context ?(nullptr_cast=false) ?(fromsource=false) =
+ let dkey = Kernel.dkey_typing_cast in
+ let origin = if fromsource then "explicit cast:" else " implicit cast:" in
+ let error msg = abort_context ("%s " ^^ msg) origin in
let rec default_rec oldt newt =
- let dkey = Kernel.dkey_typing_cast in
- let error s =
- if fromsource
- then abort_context s
- else Kernel.fatal ~current:true s
- in
match unrollType oldt, unrollType newt with
| TNamed _, _
| _, TNamed _ -> Kernel.fatal ~current:true "unrollType failed in checkCast"
@@ -6461,7 +6458,7 @@ let checkCast ?context ?(nullptr_cast=false) ?(fromsource=false) =
begin
match isTransparentUnion oldt with
| None ->
- abort_context "cast from %a to %a"
+ error "cast from %a to %a"
Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty newt
| Some _ -> ()
end
@@ -6474,8 +6471,7 @@ let checkCast ?context ?(nullptr_cast=false) ?(fromsource=false) =
| _, t1 when fromsource && not (isScalarType t1) ->
(* ISO 6.5.4.2 *)
- error "Cast over a non-scalar type %a"
- Cil_datatype.Typ.pretty newt
+ error "cast over a non-scalar type %a" Cil_datatype.Typ.pretty newt
| _ ->
error "cannot cast from %a to %a@\n"
@@ -6484,6 +6480,8 @@ let checkCast ?context ?(nullptr_cast=false) ?(fromsource=false) =
let rec castReduce fromsource force =
let dkey = Kernel.dkey_typing_cast in
+ let origin = if fromsource then "explicit cast:" else " implicit cast:" in
+ let error msg = abort_context ("%s " ^^ msg) origin in
let rec rec_default oldt newt e =
let loc = e.eloc in
let normalized_newt = type_remove_attributes_for_c_cast (unrollType newt) in
@@ -6527,7 +6525,7 @@ let rec castReduce fromsource force =
begin
match isTransparentUnion oldt with
| None ->
- abort_context "cast from %a to %a"
+ error "cast from %a to %a"
Cil_datatype.Typ.pretty oldt Cil_datatype.Typ.pretty newt
| Some fstfield ->
(* We do it now only if the expression is an lval *)
@@ -6537,8 +6535,7 @@ let rec castReduce fromsource force =
new_exp ~loc:e.eloc
(Lval (addOffsetLval (Field (fstfield, NoOffset)) lv))
| _ ->
- Kernel.fatal ~current:true
- "castTo: transparent union expression is not an lval: %a\n"
+ error "transparent union expression is not an lval: %a\n"
Cil_datatype.Exp.pretty e
in
diff --git a/tests/syntax/invalid_implicit_cast_issue_1346.i b/tests/syntax/invalid_implicit_cast_issue_1346.i
new file mode 100644
index 0000000000000000000000000000000000000000..092ce7697f66a2c31e16d355176250d26aa57506
--- /dev/null
+++ b/tests/syntax/invalid_implicit_cast_issue_1346.i
@@ -0,0 +1,15 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+char B[1];
+
+typedef void *FILE; // error: incompatible type redefinition
+typedef struct globals {
+ FILE *l;
+} T;
+
+void f(FILE *file) {
+ (*(T*)&B) = 0; // error: implicit cast: cannot cast from int to T
+}
diff --git a/tests/syntax/oracle/array_cast_bts1099.res.oracle b/tests/syntax/oracle/array_cast_bts1099.res.oracle
index 4d39dbf0d7d154c649c738f8b024cd5518ecde1d..09ba17a47e269d5a40446c613f67d7d35cd6f4fd 100644
--- a/tests/syntax/oracle/array_cast_bts1099.res.oracle
+++ b/tests/syntax/oracle/array_cast_bts1099.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing array_cast_bts1099.i (no preprocessing)
[kernel] array_cast_bts1099.i:12: User Error:
- Cast over a non-scalar type t
+ explicit cast: cast over a non-scalar type t
10 int tab1[4];
11 u* p = &tab1;
12 t* p2 = (t) p;
diff --git a/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle b/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..507b75f850f52a8e8ca5a4fbcb70fed6ce83f536
--- /dev/null
+++ b/tests/syntax/oracle/invalid_implicit_cast_issue_1346.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing invalid_implicit_cast_issue_1346.i (no preprocessing)
+[kernel] invalid_implicit_cast_issue_1346.i:14: User Error:
+ implicit cast: cannot cast from int to T
+
+ 12
+ 13 void f(FILE *file) {
+ 14 (*(T*)&B) = 0; // error: implicit cast: cannot cast from int to T
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 15 }
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/wrong-assignment.res.oracle b/tests/syntax/oracle/wrong-assignment.res.oracle
index e3ed14ddfe7d6fbd0482c6d74157fd906d72f0a4..a6f9c43d92dca9c7475fc7aaaa1761c2613f7ee7 100644
--- a/tests/syntax/oracle/wrong-assignment.res.oracle
+++ b/tests/syntax/oracle/wrong-assignment.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing wrong-assignment.i (no preprocessing)
[kernel] wrong-assignment.i:13: User Error:
- cast from ebool to _Bool
+ implicit cast: cast from ebool to _Bool
11 void d() {
12 // this assignment should be rejected
13 c.a = b;