diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index ae39644dc34dc826c772f848d058bfb6464ab3ea..a8ab10766a5e386fc3a66ccd995cb8d5f341e936 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1071,16 +1071,20 @@ struct
Cil_datatype.Logic_type.equal (Ctype ctyp1) (Ctype ctyp2)
let rec c_mk_cast ?(force=false) e oldt newt =
+ let loc = e.term_loc in
if is_same_c_type oldt newt then begin
- if force then
- Logic_utils.mk_cast ~loc:e.term_loc ~force newt e
- else e
+ if force then Logic_utils.mk_cast ~loc ~force newt e else e
end else begin
(* Watch out for constants *)
if isPointerType newt && isLogicNull e && not (isLogicZero e) then
(* \null can have any pointer type, see ACSL manual. *)
- { e with term_type = Ctype newt }
- else if isPointerType newt && isArrayType oldt && is_C_array e then begin
+ (if force then
+ Logic_const.term ~loc (TCastE (newt, e)) (Ctype newt)
+ else
+ { e with term_type = Ctype newt })
+ else if isPointerType newt && isArrayType oldt then begin
+ if not (is_C_array e) then
+ C.error loc "cannot cast logic array to pointer type";
let e = mk_logic_StartOf e in
let oldt = Logic_utils.logicCType e.term_type in
(* we have converted from array to ptr, but the pointed type might
@@ -1089,7 +1093,7 @@ struct
end else begin
match Cil.unrollType newt, e.term_node with
| TEnum (ei,[]), TConst (LEnum { eihost = ei'})
- when ei.ename = ei'.ename -> e
+ when ei.ename = ei'.ename && not force -> e
| _ ->
{ e with term_node =
(Logic_utils.mk_cast ~force newt e).term_node;
@@ -1196,10 +1200,20 @@ struct
in
lift_set convert_one_location t
- let rec mk_cast e newt =
+ let rec mk_cast ?(explicit=false) e newt =
+ let force = explicit in
let loc = e.term_loc in
- if is_same_type e.term_type newt then e
- else if is_enum_cst e newt then e
+ let truncate_info =
+ List.hd @@ Logic_env.find_all_logic_functions "\\truncate"
+ in
+ if is_same_type e.term_type newt then begin
+ if explicit then begin
+ match Logic_const.unroll_ltdef newt with
+ | Ctype cnewt ->
+ { e with term_node = TCastE(cnewt,e); term_type = newt }
+ | _ -> e
+ end else e
+ end else if is_enum_cst e newt then { e with term_type = newt }
else begin
match
(unroll_type e.term_type),
@@ -1207,15 +1221,16 @@ struct
(Logic_const.unroll_ltdef newt)
with
| Ctype oldt, Ctype newt ->
- c_mk_cast e oldt newt
+ c_mk_cast ~force e oldt newt
| t1, Ltype ({lt_name = name},[])
when name = Utf8_logic.boolean && is_integral_type t1 ->
- { e with
- term_node =
- TBinOp(Cil_types.Ne,
- mk_cast e Linteger,
- lzero ~loc ());
- term_type = Ltype(C.find_logic_type Utf8_logic.boolean,[]) }
+ let t2 = Ltype (C.find_logic_type Utf8_logic.boolean,[]) in
+ { e with term_node = TLogic_coerce(t2,e); term_type = t2 }
+ | t1, Linteger when Logic_const.is_boolean_type t1 ->
+ logic_coerce Linteger e
+ | t1, Ctype t2 when Logic_const.is_boolean_type t1
+ && is_integral_type newt ->
+ Logic_const.term ~loc (TCastE (t2,e)) newt
| ty1, Ltype({lt_name="set"},[ty2])
when is_pointer_type ty1 &&
is_plain_pointer_type ty2 &&
@@ -1224,27 +1239,37 @@ struct
| Ltype({lt_name = "set"},[_]), Ltype({lt_name="set"},[ty2]) ->
let e = lift_set (fun e -> mk_cast e ty2) e in
{ e with term_type = make_set_type e.term_type}
+ (* extremely dirty cast to allow Eva to understand some libc
+ specifications *)
+ | Ltype({lt_name = "set"},[_]), Ctype ty2 when explicit ->
+ Logic_utils.mk_cast ~loc ty2 e
| _ , Ltype({lt_name = "set"},[ ty2 ]) ->
let e = mk_cast e ty2 in
logic_coerce (make_set_type e.term_type) e
| Linteger, Linteger | Lreal, Lreal -> e
| Linteger, Ctype t when isLogicPointerType newt && isLogicNull e ->
- c_mk_cast e intType t
+ c_mk_cast ~force e intType t
+ | Linteger, (Ctype newt) | Lreal, (Ctype newt) when explicit ->
+ Logic_utils.mk_cast ~loc newt e
| Linteger, Ctype t when isIntegralType t ->
- (try
- C.integral_cast t e
- with Failure s -> C.error loc "%s" s)
+ (try C.integral_cast t e with Failure s -> C.error loc "%s" s)
| Linteger, Ctype _ | Lreal, Ctype _ ->
C.error loc "invalid implicit cast from %a to C type %a"
Cil_printer.pp_logic_type e.term_type
Cil_printer.pp_logic_type newt
| Ctype t, Linteger when Cil.isIntegralType t -> logic_coerce Linteger e
+ | Ctype t, Linteger when Cil.isArithmeticType t && explicit ->
+ Logic_const.term
+ ~loc (Tapp(truncate_info,[], [logic_coerce Lreal e])) Linteger
| Ctype t, Lreal when isArithmeticType t -> logic_coerce Lreal e
| Ctype _, (Lreal | Linteger) ->
C.error loc "invalid implicit cast from %a to logic type %a"
Cil_printer.pp_logic_type e.term_type
Cil_printer.pp_logic_type newt
| Linteger, Lreal -> logic_coerce Lreal e
+ | Lreal, Linteger when explicit ->
+ let term_node = Tapp(truncate_info,[],[e]) in
+ Logic_const.term ~loc term_node Linteger
| Lreal, Linteger ->
C.error loc
"invalid cast from real to integer. \
@@ -2838,57 +2863,9 @@ struct
| PLcast (ty, t) ->
let t = term env t in
(* no casts of tsets in grammar *)
- let ct =
- Logic_const.unroll_ltdef (logic_type ctxt loc env ty)
- in
- (match ct with
- | (Ctype tnew) ->
- (match t.term_type with
- | Ctype told ->
- if isPointerType tnew && isArrayType told
- && not (is_C_array t) then
- ctxt.error loc "cannot cast logic array to pointer type";
- if Cil.isVoidPtrType told then
- (Logic_utils.mk_cast tnew t).term_node, ct
- else
- (c_mk_cast ~force:true t told tnew).term_node , ct
- | _ -> (Logic_utils.mk_cast tnew t).term_node, ct)
- | Linteger when is_arithmetic_type t.term_type ->
- let truncate_info =
- List.hd @@ Logic_env.find_all_logic_functions "\\truncate"
- in
- let term_node =
- match unroll_type t.term_type with
- | Lreal -> Tapp (truncate_info, [], [t])
- | Ctype ty when not (Cil.isIntegralType ty) ->
- (* arithmetic but not integral type: floating point.
- Coerce to real before applying truncate. *)
- Tapp (
- truncate_info, [],
- [ Logic_const.term ~loc:t.term_loc
- (TLogic_coerce(Lreal,t)) Lreal ])
- | Ctype _ ->
- (* an integral type by construction *)
- TLogic_coerce(Linteger, t)
- | Linteger -> (* coercion is a no-op. *) t.term_node
- | Ltype _ | Lvar _ | Larrow _ as ty ->
- Kernel.fatal
- "%a should not be considered an arithmetic type"
- Cil_printer.pp_logic_type ty
- in
- term_node, Linteger
- | Ltype _ | Lvar _ | Larrow _
- when Logic_utils.is_same_type t.term_type ct -> (* cast from T to T *)
- t.term_node, t.term_type
- | Ltype (_,[]) when Logic_const.is_boolean_type ct &&
- Cil.isLogicIntegralType t.term_type ->
- TLogic_coerce(ct, t), ct (* cast from integral type to boolean *)
- | Linteger when Logic_const.is_boolean_type t.term_type ->
- TLogic_coerce(ct, t), ct (* cast from boolean to integer *)
- | Linteger | Lreal | Ltype _ | Lvar _ | Larrow _ ->
- ctxt.error loc "cannot cast from %a to %a"
- Cil_printer.pp_logic_type t.term_type
- Cil_printer.pp_logic_type ct)
+ let ct = Logic_const.unroll_ltdef (logic_type ctxt loc env ty) in
+ let { term_node; term_type } = mk_cast ~explicit:true t ct in
+ (term_node, term_type)
| PLcoercion (t,ty) ->
let t = term env t in
(match Logic_const.unroll_ltdef (logic_type ctxt loc env ty) with
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 59d1fc9037353595777fb5883510555e39d98678..f30df04280448362252376dfc6aa835029466b64 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -291,8 +291,14 @@ sig
val type_of_field:
location -> string -> logic_type -> (term_offset * logic_type)
- (** @since Nitrogen-20111001 *)
- val mk_cast: Cil_types.term -> Cil_types.logic_type -> Cil_types.term
+ (**
+ @param explicit true if the cast is present in original source.
+ defaults to false
+ @since Nitrogen-20111001
+ @modify Frama-C+dev introduces explicit param
+ *)
+ val mk_cast:
+ ?explicit:bool -> Cil_types.term -> Cil_types.logic_type -> Cil_types.term
(** type-checks a term. *)
val term : Lenv.t -> Logic_ptree.lexpr -> term