diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 953c0e68aca05f8b62e83ef531a97f8922ae892e..4c70e7912aa6f3fc37ee63b1e160179b3874ed1b 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1368,7 +1368,7 @@ let rec is_boolean_result e = (* Like Cil.mkCastT, but it calls typeForInsertedCast *) let makeCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) = if need_cast oldt newt then - Cil.mkCastT e oldt (!typeForInsertedCast e oldt newt) + Cil.mkCastT oldt (!typeForInsertedCast e oldt newt) e else e let makeCast ~(e: exp) ~(newt: typ) = @@ -2652,8 +2652,8 @@ let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ = evaluate them. Check first machine independent comparison. *) let checkEqualSize (machdep: bool) = let size_t = Cil.theMachine.Cil.typeOfSizeOf in - let size_t_oldsz' = Cil.mkCast ~force:false ~e:oldsz' ~newt:size_t in - let size_t_sz' = Cil.mkCast ~force:false ~e:sz' ~newt:size_t in + let size_t_oldsz' = Cil.mkCast ~force:false ~newt:size_t oldsz' in + let size_t_sz' = Cil.mkCast ~force:false ~newt:size_t sz' in ExpStructEq.equal (constFold machdep size_t_oldsz') (constFold machdep size_t_sz') @@ -2852,7 +2852,7 @@ let rec castTo ?context ?(fromsource=false) end else begin let nt' = if fromsource then nt' else !typeForInsertedCast e ot' nt' in let result = (nt', if theMachine.insertImplicitCasts || fromsource then - Cil.mkCastT ~force:true ~e ~oldt:ot ~newt:nt' else e) + Cil.mkCastT ~force:true ~oldt:ot ~newt:nt' e else e) in let error s = if fromsource then abort_context s else Kernel.fatal ~current:true s @@ -2872,10 +2872,10 @@ let rec castTo ?context ?(fromsource=false) else nt, Cil.mkCastT + ot nt' (constFold true (new_exp ~loc:e.eloc (BinOp(Ne,e,Cil.integer ~loc:e.eloc 0,intType)))) - ot nt' | TInt(_,_), TInt(_,_) -> (* We used to ignore attributes on integer-integer casts. Not anymore *) (* if ikindo = ikindn then (nt, e) else *) diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml index 99e2cef1c2ea23922820e87c639dfb55749c480d..e0e3cd3ea286fc152a9a4371adca76fb0b470a36 100644 --- a/src/kernel_services/analysis/destructors.ml +++ b/src/kernel_services/analysis/destructors.ml @@ -32,7 +32,7 @@ let add_destructor (_, l as acc) var = let e = match Globals.Functions.get_params kf with | vi :: _ -> - if Cil.need_cast (Cil.typeOf e) vi.vtype then Cil.mkCast e vi.vtype + if Cil.need_cast (Cil.typeOf e) vi.vtype then Cil.mkCast vi.vtype e else e | [] -> Kernel.fatal diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml index 06a027ae6107987adb4143b0eb3879b2c455fbde..98cf45da1bd0c70c4b39f8ff3fc5e3d6fc8b56f0 100644 --- a/src/kernel_services/analysis/logic_interp.ml +++ b/src/kernel_services/analysis/logic_interp.ml @@ -312,7 +312,7 @@ and loc_to_exp ~result {term_node = lnode ; term_type = ltype; term_loc = loc} = Logic_utils.is_same_type (Logic_typing.type_of_set_elem set) t.term_type -> loc_to_exp ~result t - | Tnull -> [ Cil.mkCast (Cil.zero ~loc) (TPtr(TVoid [], [])) ] + | Tnull -> [ Cil.mkCast (TPtr(TVoid [], [])) (Cil.zero ~loc) ] (* additional constructs *) | Tapp _ | Tlambda _ | Trange _ | Tlet _ diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml index eefbda4d0b28f0b9c96d180dd9057dad295006d4..f2edb73c5dc8aaf1cf8d174da8c3c1150b4816fe 100644 --- a/src/kernel_services/ast_data/alarms.ml +++ b/src/kernel_services/ast_data/alarms.ml @@ -648,7 +648,7 @@ let create_predicate ?(loc=Location.unknown) alarm = | TPtr (TFun (ret, None, var, attrs), _), Some args -> let ltyps = List.map (fun arg -> "", Cil.typeOf arg, []) args in let typ = TFun (ret, Some ltyps, var, attrs) in - Cil.mkCast e (TPtr (typ, [])) + Cil.mkCast (TPtr (typ, [])) e | t', _ -> Kernel.fatal "Trying to emit a Function_pointer alarm over expression %a \ diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index 63e9bbc9a072dfc6b7a3e54751e03e526a397b4f..16c6894269008fd2963deac0ddf984fdeb486002 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -5757,7 +5757,7 @@ let getCompField cinfo fieldName = (fun fi -> fi.fname = fieldName) (Option.value ~default:[] cinfo.cfields) -let mkCastT ?(force=false) ~(e: exp) ~(oldt: typ) ~(newt: typ) = +let mkCastT ?(force=false) ~(oldt: typ) ~(newt: typ) e = let loc = e.eloc in (* Issue #!1546 let force = force || @@ -5794,8 +5794,8 @@ let mkCastT ?(force=false) ~(e: exp) ~(oldt: typ) ~(newt: typ) = end else e -let mkCast ?force ~(e: exp) ~(newt: typ) = - mkCastT ?force ~e ~oldt:(typeOf e) ~newt +let mkCast ?force ~(newt: typ) e = + mkCastT ?force ~oldt:(typeOf e) ~newt e (* TODO: unify this with doBinOp in Cabs2cil. *) let mkBinOp ~loc op e1 e2 = @@ -5804,8 +5804,8 @@ let mkBinOp ~loc op e1 e2 = let machdep = false in let make_expr common_type res_type = constFoldBinOp ~loc machdep op - (mkCastT e1 t1 common_type) - (mkCastT e2 t2 common_type) + (mkCastT t1 common_type e1) + (mkCastT t2 common_type e2) res_type in let doArithmetic () = @@ -5826,7 +5826,7 @@ let mkBinOp ~loc op e1 e2 = let compare_pointer op ?cast1 ?cast2 e1 e2 = let do_cast e = function | None -> e - | Some t' -> mkCastT ~force:false ~e ~oldt:(typeOf e) ~newt:t' + | Some t' -> mkCastT ~force:false ~oldt:(typeOf e) ~newt:t' e in let e1, e2 = if need_cast ~force:true (typeOf e1) (typeOf e2) then @@ -5857,14 +5857,14 @@ let mkBinOp ~loc op e1 e2 = let t1' = integralPromotion t1 in let t2' = integralPromotion t2 in constFoldBinOp ~loc machdep op - (mkCastT e1 t1 t1') (mkCastT e2 t2 t2') t1' + (mkCastT t1 t1' e1) (mkCastT t2 t2' e2) t1' | (PlusA|MinusA) when isArithmeticType t1 && isArithmeticType t2 -> doArithmetic () | (PlusPI|MinusPI|IndexPI) when isPointerType t1 && isIntegralType t2 -> constFoldBinOp ~loc machdep op e1 e2 t1 | MinusPP when isPointerType t1 && isPointerType t2 -> (* NB: Same as cabs2cil. Check if this is really what the standard says*) - constFoldBinOp ~loc machdep op e1 (mkCastT e2 t2 t1) intType + constFoldBinOp ~loc machdep op e1 (mkCastT t2 t1 e2) intType | (Eq|Ne|Lt|Le|Ge|Gt) when isArithmeticType t1 && isArithmeticType t2 -> doArithmeticComp () @@ -5894,8 +5894,8 @@ let mkBinOp_safe_ptr_cmp ~loc op e1 e2 = if isPointerType t1 && isPointerType t2 && not (isZero e1) && not (isZero e2) then begin - mkCast ~force:true ~e:e1 ~newt:theMachine.upointType, - mkCast ~force:true ~e:e2 ~newt:theMachine.upointType + mkCast ~force:true ~newt:theMachine.upointType e1, + mkCast ~force:true ~newt:theMachine.upointType e2 end else e1, e2 | _ -> e1, e2 in @@ -6013,7 +6013,7 @@ let rec makeZeroInit ~loc (t: typ) : init = | TPtr _ as t -> SingleInit( - if theMachine.insertImplicitCasts then mkCast (zero ~loc) t + if theMachine.insertImplicitCasts then mkCast t (zero ~loc) else zero ~loc) | x -> Kernel.fatal ~current:true "Cannot initialize type: %a" !pp_typ_ref x diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index ae92a0c24ed9f2fa5bb8db649f1a52031fee9632..3e7d875bf35d442a050f313ce5198e930c0373b2 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -978,11 +978,14 @@ val need_cast: ?force:bool -> typ -> typ -> bool type is the same as the old type, then no cast is added, unless [force] is [true] (default is [false]) @modify Fluorine-20130401 add [force] argument + @modify Frama-C+dev change order or arguments *) -val mkCastT: ?force:bool -> e:exp -> oldt:typ -> newt:typ -> exp +val mkCastT: ?force:bool -> oldt:typ -> newt:typ -> exp -> exp -(** Like {!Cil.mkCastT} but uses typeOf to get [oldt] *) -val mkCast: ?force:bool -> e:exp -> newt:typ -> exp +(** Like {!Cil.mkCastT} but uses typeOf to get [oldt] + @modify Frama-C+dev change order or arguments +*) +val mkCast: ?force:bool -> newt:typ -> exp -> exp (** Equivalent to [stripCasts] for terms. *) val stripTermCasts: term -> term diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml index ab3fa392e9d2b53efb783f0f8661a9a69802a50d..5edc8c843924ecd4158d1fb2a90700fa2c672bb3 100644 --- a/src/plugins/constant_propagation/api.ml +++ b/src/plugins/constant_propagation/api.ml @@ -93,7 +93,7 @@ class propagate project fnames ~cast_intro = object(self) else oldt, newt in - let exp = Cil.mkCastT e oldt newt in + let exp = Cil.mkCastT oldt newt e in if cast_intro then exp else match exp.enode with diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml index ebac4f3a70f0e9ee966a874f44e52e60225ba20a..ebb75d0b2b7cda9a7955284269fcb74cab8f1041 100644 --- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml +++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml @@ -320,7 +320,7 @@ let tapp_to_exp ~loc fname env kf t li params_ty args = the exact type of the parameter is only computed when the function is generated *) List.map2 - (fun (_, newt, _) e -> Cil.mkCast ~force:false ~newt ~e) + (fun (_, newt, _) e -> Cil.mkCast ~force:false ~newt e) params args | _ -> assert false diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml index 0af7f3b0697137395bd885f1e88f797bc4943209..b0af08300c4d904bf229f0123eccca0587004951 100644 --- a/src/plugins/e-acsl/src/code_generator/rational.ml +++ b/src/plugins/e-acsl/src/code_generator/rational.ml @@ -170,7 +170,7 @@ let add_cast ~loc ?name e env kf ty = let e, env = get_double e env in Options.warning ~once:true "R to float: double rounding might cause unsoundness"; - Cil.mkCastT ~force:false ~e ~oldt:Cil.doubleType ~newt:ty, env + Cil.mkCastT ~force:false ~oldt:Cil.doubleType ~newt:ty e, env | TInt(IULongLong, _) -> (* The biggest C integer type we can extract from GMP is ulong *) Error.not_yet "R to unsigned long long" diff --git a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml index 2c3497df87388788c01f9b46c4b751bb24bc240f..c126fe01e0ba9fbff3662f5e8bd225919a71245a 100644 --- a/src/plugins/e-acsl/src/code_generator/smart_stmt.ml +++ b/src/plugins/e-acsl/src/code_generator/smart_stmt.ml @@ -81,7 +81,7 @@ let do_call ~loc ?result vi args = | TPtr _, TArray _, _ -> assert false | _, _, _ -> arg in - let e = Cil.mkCast ~force:false ~newt:ty ~e in + let e = Cil.mkCast ~force:false ~newt:ty e in make_rev_args (e :: res) args_tl param_ty_tl | arg :: args_tl, [] when variadic -> make_rev_args (arg :: res) args_tl [] | [], [] -> res diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml index 960cddb412e78a632121512474dde0894afc113a..5f34444f061e2c48b355d045a491c35313525344 100644 --- a/src/plugins/e-acsl/src/code_generator/translate.ml +++ b/src/plugins/e-acsl/src/code_generator/translate.ml @@ -108,7 +108,7 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e = only non integral value that can be seen as an integer, while the type system infers that it is C-representable (see tests/runtime/null.i) *) - Cil.mkCast e Cil.longType (* \null *) + Cil.mkCast Cil.longType e (* \null *) else e in @@ -147,7 +147,7 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e = Rational.add_cast ~loc ?name e env kf ctx else (* C type --> another C type *) - Cil.mkCastT ~force:false ~e ~oldt:ty ~newt:ctx, env + Cil.mkCastT ~force:false ~oldt:ty ~newt:ctx e, env let constant_to_exp ~loc t c = let mk_real s = @@ -733,7 +733,7 @@ and context_insensitive_term_to_exp kf env t = e, env, C_number, name | Tblock_length _ -> Env.not_yet env "labeled \\block_length" | Tnull -> - Cil.mkCast (Cil.zero ~loc) (TPtr(TVoid [], [])), env, C_number, "null" + Cil.mkCast (TPtr(TVoid [], [])) (Cil.zero ~loc), env, C_number, "null" | TUpdate _ -> Env.not_yet env "functional update" | Ttypeof _ -> Env.not_yet env "typeof" | Ttype _ -> Env.not_yet env "C type" diff --git a/src/plugins/instantiate/basic_blocks.ml b/src/plugins/instantiate/basic_blocks.ml index 87f9f09c8791f66d593e0ea00dc3f892978f25c5..2511974748e1115c3103097ce958fe3ff0016f01 100644 --- a/src/plugins/instantiate/basic_blocks.ml +++ b/src/plugins/instantiate/basic_blocks.ml @@ -45,7 +45,7 @@ let call_function lval vi args = let typs = Cil.argsToList typs in let gen_arg exp (_, typ, _) = if Cil_datatype.Typ.equal vi.vtype typ then exp - else Cil.mkCast exp typ + else Cil.mkCast typ exp in let args = List.map2 gen_arg args typs in Call(lval, (Cil.evar vi), args, loc) diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml index 92c47cab940c34d00e779f4c8f4e02a71e6f304e..bb3ce6ca4d87e11a6f6db75609d4ea3ed7aec3b9 100644 --- a/src/plugins/instantiate/string/memset.ml +++ b/src/plugins/instantiate/string/memset.ml @@ -253,7 +253,7 @@ let retype_args (_t, e) args = | Value_of t -> base_char_type t | _ -> unexpected "trying to retype arguments on an ill-typed call" in - let v = Cil.mkCast (Cil.stripCasts v) base_type in + let v = Cil.mkCast base_type (Cil.stripCasts v) in [ ptr ; v ; n ] | Some fv, [ ptr ; v ; n ] -> let ptr = Cil.stripCasts ptr in diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml index 6a31f40a376c9bebb12bd3bab67714ca9bb6725a..436f349721f7e939855f61023a623740b4aeb0f0 100644 --- a/src/plugins/value/utils/value_util.ml +++ b/src/plugins/value/utils/value_util.ml @@ -186,7 +186,7 @@ let zero e = | TPtr _ -> let ik = Cil.(theMachine.upointKind) in let zero = Cil.new_exp ~loc (Const (CInt64 (Integer.zero, ik, None))) in - Cil.mkCast ~force:true ~e:zero ~newt:typ + Cil.mkCast ~force:true ~newt:typ zero | typ -> Value_parameters.fatal ~current:true "non-scalar type %a" Printer.pp_typ typ diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml index 586d6041d62af0615c852996638b45362bfb81e5..2964a64b64858b55680f17407f77b7920984f351 100644 --- a/src/plugins/variadic/generic.ml +++ b/src/plugins/variadic/generic.ml @@ -120,7 +120,7 @@ let translate_va_builtin caller inst = (* Build the replacing instruction *) let mk_lval_exp lval = Cil.new_exp ~loc (Lval lval) in let mk_mem exp = mk_lval_exp (Cil.mkMem ~addr:exp ~off:NoOffset) in - let mk_cast exp typ = Cil.mkCast ~force:false ~e:exp ~newt:typ in + let mk_cast exp typ = Cil.mkCast ~force:false ~newt:typ exp in let src = mk_mem (mk_cast (mk_mem (mk_lval_exp va_list)) (TPtr (typ,[]))) in [ Set (lval, src, loc); @@ -173,7 +173,7 @@ let translate_call ~fundec ~ghost block loc mk_call callee pars = (* Translate the call *) let exp_vargs = Cil.mkAddrOrStartOf ~loc (Cil.var vargs) in - let new_arg = Cil.mkCast ~force:false ~e:exp_vargs ~newt:(vpar_typ []) in + let new_arg = Cil.mkCast ~force:false ~newt:(vpar_typ []) exp_vargs in let new_args = s_exps @ [new_arg] @ g_exps in let call = mk_call callee new_args in instrs @ [call] diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml index 1db894c1d19b942e2cdf30e141e92f11ab772613..f2191e807b66351eac769dcfae28502b5176d8e2 100644 --- a/src/plugins/variadic/standard.ml +++ b/src/plugins/variadic/standard.ml @@ -134,7 +134,7 @@ let cast_arg i paramtyp exp = (i + 1) pretty_typ argtyp pretty_typ paramtyp end; - Cil.mkCast ~force:false ~e:exp ~newt:paramtyp + Cil.mkCast ~force:false ~newt:paramtyp exp (* cast a list of args to the tparams list of types and remove unused args *) diff --git a/tests/cil/mkBinOp.ml b/tests/cil/mkBinOp.ml index be2c8fefa7ea2cf19a2bf6c68c63c18105eca87f..7ef013171d3ffcb3393faadca7654fcbb964c638 100644 --- a/tests/cil/mkBinOp.ml +++ b/tests/cil/mkBinOp.ml @@ -5,19 +5,19 @@ let loc = Location.unknown let null () = let e = zero ~loc in - mkCast ~force:true ~e ~newt:voidPtrType + mkCast ~force:true ~newt:voidPtrType e let inull () = let e = zero ~loc in - mkCast ~force:true ~e ~newt:intPtrType + mkCast ~force:true ~newt:intPtrType e let cone () = let e = one ~loc in - mkCast ~force:true ~e ~newt:charPtrType + mkCast ~force:true ~newt:charPtrType e let ione () = let e = one ~loc in - mkCast ~force:true ~e ~newt:intPtrType + mkCast ~force:true ~newt:intPtrType e let test = let n = ref 0 in