diff --git a/infer/src/IR/Cfg.ml b/infer/src/IR/Cfg.ml index 2eba34e63..cc1d49723 100644 --- a/infer/src/IR/Cfg.ml +++ b/infer/src/IR/Cfg.ml @@ -85,15 +85,15 @@ let inline_synthetic_method ((ret_id, _) as ret) etl pdesc loc_call : Sil.instr {id= ret_id; e= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt; typ; loc= loc_call} in found instr instr' - | ( Sil.Store {e1= Exp.Lfield (_, fn, ft); root_typ= bt} + | ( Sil.Store {e1= Exp.Lfield (_, fn, ft); root_typ; typ} , [(* setter for fields *) (e1, _); (e2, _)] ) -> - let instr' = Sil.Store {e1= Exp.Lfield (e1, fn, ft); root_typ= bt; e2; loc= loc_call} in + let instr' = Sil.Store {e1= Exp.Lfield (e1, fn, ft); root_typ; typ; e2; loc= loc_call} in found instr instr' - | Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt}, [(e1, _)] + | Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ; typ}, [(e1, _)] when Pvar.is_global pvar -> (* setter for static fields *) let instr' = - Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt; e2= e1; loc= loc_call} + Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ; typ; e2= e1; loc= loc_call} in found instr instr' | Sil.Call (_, Exp.Const (Const.Cfun pn), etl', _, cf), _ diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index 5a901a039..9e129e5d1 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -50,12 +50,17 @@ type instr = The [root_typ] is deprecated: it is broken in C/C++. We are removing [root_typ] in the future, so please use [typ] instead. *) - | Store of {e1: Exp.t; root_typ: Typ.t; e2: Exp.t; loc: Location.t} + | Store of {e1: Exp.t; root_typ: Typ.t; typ: Typ.t; e2: Exp.t; loc: Location.t} (** Store the value of an expression into the heap. - [*exp1:root_typ = exp2] where + + [*exp1:typ(root_typ) = exp2] where [exp1] is an expression denoting a heap address + [typ] is typ of [*exp1] and [exp2] [root_typ] is the root type of [exp1] - [exp2] is the expression whose value is stored. *) + [exp2] is the expression whose value is stored. + + The [root_typ] is deprecated: it is broken in C/C++. We are removing [root_typ] in the + future, so please use [typ] instead. *) | Prune of Exp.t * Location.t * bool * if_kind (** prune the state based on [exp=1], the boolean indicates whether true branch *) | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t @@ -415,17 +420,17 @@ let pp_instr_metadata pe f = function let pp_instr ~print_types pe0 f instr = let pp_typ = if print_types then Typ.pp_full else Typ.pp in + let pp_root ~typ ~root_typ f = + if not (Typ.equal typ root_typ) then F.fprintf f "(root %a)" (pp_typ pe0) root_typ + in color_wrapper pe0 f instr ~f:(fun pe f instr -> match instr with | Load {id; e; root_typ; typ; loc} -> - let pp_root f = - if not (Typ.equal typ root_typ) then F.fprintf f "(root %a)" (pp_typ pe0) root_typ - in F.fprintf f "%a=*%a:%a%t [%a]" Ident.pp id (pp_exp_printenv ~print_types pe) e - (pp_typ pe0) typ pp_root Location.pp loc - | Store {e1; root_typ; e2; loc} -> - F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) root_typ - (pp_exp_printenv ~print_types pe) e2 Location.pp loc + (pp_typ pe0) typ (pp_root ~typ ~root_typ) Location.pp loc + | Store {e1; root_typ; typ; e2; loc} -> + F.fprintf f "*%a:%a%t=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) root_typ + (pp_root ~typ ~root_typ) (pp_exp_printenv ~print_types pe) e2 Location.pp loc | Prune (cond, loc, true_branch, _) -> F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv ~print_types pe) cond true_branch Location.pp loc @@ -1280,11 +1285,11 @@ let instr_sub_ids ~sub_id_binders f instr = let rhs_exp' = exp_sub_ids f rhs_exp in if phys_equal id' id && phys_equal rhs_exp' rhs_exp then instr else Load {id= id'; e= rhs_exp'; root_typ; typ; loc} - | Store {e1= lhs_exp; root_typ; e2= rhs_exp; loc} -> + | Store {e1= lhs_exp; root_typ; typ; e2= rhs_exp; loc} -> let lhs_exp' = exp_sub_ids f lhs_exp in let rhs_exp' = exp_sub_ids f rhs_exp in if phys_equal lhs_exp' lhs_exp && phys_equal rhs_exp' rhs_exp then instr - else Store {e1= lhs_exp'; root_typ; e2= rhs_exp'; loc} + else Store {e1= lhs_exp'; root_typ; typ; e2= rhs_exp'; loc} | Call (((id, typ) as ret_id_typ), fun_exp, actuals, call_flags, loc) -> let ret_id' = if sub_id_binders then diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index 2d00a236c..8879ce043 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -48,12 +48,17 @@ type instr = The [root_typ] is deprecated: it is broken in C/C++. We are removing [root_typ] in the future, so please use [typ] instead. *) - | Store of {e1: Exp.t; root_typ: Typ.t; e2: Exp.t; loc: Location.t} + | Store of {e1: Exp.t; root_typ: Typ.t; typ: Typ.t; e2: Exp.t; loc: Location.t} (** Store the value of an expression into the heap. - [*exp1:root_typ = exp2] where + + [*exp1:typ(root_typ) = exp2] where [exp1] is an expression denoting a heap address + [typ] is typ of [*exp1] and [exp2] [root_typ] is the root type of [exp1] - [exp2] is the expression whose value is stored. *) + [exp2] is the expression whose value is stored. + + The [root_typ] is deprecated: it is broken in C/C++. We are removing [root_typ] in the + future, so please use [typ] instead. *) | Prune of Exp.t * Location.t * bool * if_kind (** prune the state based on [exp=1], the boolean indicates whether true branch *) | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t diff --git a/infer/src/IR/SpecializeProcdesc.ml b/infer/src/IR/SpecializeProcdesc.ml index 26035a927..a40278dde 100644 --- a/infer/src/IR/SpecializeProcdesc.ml +++ b/infer/src/IR/SpecializeProcdesc.ml @@ -88,7 +88,11 @@ let with_formals_types_proc callee_pdesc resolved_pdesc substitutions = | Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= origin_exp; loc} -> let set_instr = Sil.Store - {e1= convert_exp assignee_exp; root_typ= origin_typ; e2= convert_exp origin_exp; loc} + { e1= convert_exp assignee_exp + ; root_typ= origin_typ + ; typ= origin_typ + ; e2= convert_exp origin_exp + ; loc } in Some set_instr | Sil.Call @@ -235,12 +239,18 @@ let with_block_args_instrs resolved_pdesc substitutions = get_block_name_and_load_captured_vars_instrs block_param loc in let closure = Exp.Closure {name= block_name; captured_vars= id_exp_typs} in - let instr = Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= closure; loc} in + let instr = + Sil.Store {e1= assignee_exp; root_typ= origin_typ; typ= origin_typ; e2= closure; loc} + in ((remove_temps_instr :: instr :: load_instrs) @ instrs, id_map) | Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= origin_exp; loc} -> let set_instr = Sil.Store - {e1= convert_exp assignee_exp; root_typ= origin_typ; e2= convert_exp origin_exp; loc} + { e1= convert_exp assignee_exp + ; root_typ= origin_typ + ; typ= origin_typ + ; e2= convert_exp origin_exp + ; loc } in (set_instr :: instrs, id_map) | Sil.Call (return_ids, Exp.Var id, origin_args, loc, call_flags) -> ( diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index a9f57f61a..e9e1fd306 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -19,7 +19,7 @@ let execute___builtin_va_arg {Builtin.summary; tenv; prop_; path; args; loc; exe Builtin.ret_typ = match args with | [(lexp3, typ3)] -> - let instr' = Sil.Store {e1= lexp3; root_typ= typ3; e2= Exp.zero; loc} in + let instr' = Sil.Store {e1= lexp3; root_typ= typ3; typ= typ3; e2= Exp.zero; loc} in SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton instr') [(prop_, path)] | _ -> @@ -627,7 +627,11 @@ let execute___cxx_typeid ({Builtin.summary; tenv; prop_; args; loc; exe_env} as let typ_string = Typ.to_string typ in let set_instr = Sil.Store - {e1= field_exp; root_typ= Typ.mk Tvoid; e2= Exp.Const (Const.Cstr typ_string); loc} + { e1= field_exp + ; root_typ= Typ.mk Tvoid + ; typ= Typ.mk Tvoid + ; e2= Exp.Const (Const.Cstr typ_string) + ; loc } in SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) res | _ -> @@ -767,6 +771,7 @@ let execute___infer_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_env Sil.Store { e1= Exp.Lvar Sil.custom_error ; root_typ= Typ.mk Tvoid + ; typ= Typ.mk Tvoid ; e2= Exp.Const (Const.Cstr error_str) ; loc } in @@ -787,6 +792,7 @@ let execute___assert_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_en Sil.Store { e1= Exp.Lvar Sil.custom_error ; root_typ= Typ.mk Tvoid + ; typ= Typ.mk Tvoid ; e2= Exp.Const (Const.Cstr error_str) ; loc } in diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index 527a2c534..c22ba6833 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -41,7 +41,7 @@ let compound_assignment_binary_operation_instruction boi_kind (e1, t1) typ e2 lo in let id = Ident.create_fresh Ident.knormal in [ Sil.Load {id; e= e1; root_typ= typ; typ; loc} - ; Sil.Store {e1; root_typ= typ; e2= Exp.BinOp (bop, Exp.Var id, e2); loc} ] + ; Sil.Store {e1; root_typ= typ; typ; e2= Exp.BinOp (bop, Exp.Var id, e2); loc} ] in (e1, instrs) @@ -105,7 +105,7 @@ let binary_operation_instruction source_range boi ((e1, t1) as e1_with_typ) typ | `LOr -> (binop_exp Binop.LOr, []) | `Assign -> - (e1, [Sil.Store {e1; root_typ= typ; e2; loc}]) + (e1, [Sil.Store {e1; root_typ= typ; typ; e2; loc}]) | `Cmp -> CFrontend_errors.unimplemented __POS__ source_range "C++20 spaceship operator <=>" (* C++20 spaceship operator <=>, TODO *) @@ -132,7 +132,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc = let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in - (Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_plus_1; loc}]) + (Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; typ; e2= e_plus_1; loc}]) | `PreInc -> let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in @@ -141,7 +141,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc = let exp = if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_plus_1 in - (exp, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_plus_1; loc}]) + (exp, [instr1; Sil.Store {e1= e; root_typ= typ; typ; e2= e_plus_1; loc}]) | `PostDec -> let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in @@ -149,7 +149,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc = if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ) in let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in - (Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_minus_1; loc}]) + (Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; typ; e2= e_minus_1; loc}]) | `PreDec -> let id = Ident.create_fresh Ident.knormal in let instr1 = Sil.Load {id; e; root_typ= typ; typ; loc} in @@ -160,7 +160,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc = let exp = if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_minus_1 in - (exp, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_minus_1; loc}]) + (exp, [instr1; Sil.Store {e1= e; root_typ= typ; typ; e2= e_minus_1; loc}]) | `Not -> (un_exp Unop.BNot, []) | `Minus -> diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index bdbc4f600..7d0bb5829 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -423,7 +423,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s |> mk_trans_result exp_typ | Tint _ | Tfloat _ | Tptr _ -> let zero_exp = Exp.zero_of_type_exn typ in - let instrs = [Sil.Store {e1= exp; root_typ= typ; e2= zero_exp; loc= sil_loc}] in + let instrs = [Sil.Store {e1= exp; root_typ= typ; typ; e2= zero_exp; loc= sil_loc}] in mk_trans_result (exp, typ) {empty_control with instrs} | Tfun _ | Tvoid | Tarray _ | TVar _ -> CFrontend_errors.unimplemented __POS__ stmt_info.Clang_ast_t.si_source_range @@ -1506,7 +1506,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s e' in let temp_var = Exp.Lvar pvar in - let set_temp_var = [Sil.Store {e1= temp_var; root_typ= var_typ; e2= e'; loc= sil_loc}] in + let set_temp_var = + [Sil.Store {e1= temp_var; root_typ= var_typ; typ= var_typ; e2= e'; loc= sil_loc}] + in let temp_return = (temp_var, var_typ) in let tmp_var_res_trans = mk_trans_result temp_return {empty_control with instrs= set_temp_var} @@ -2327,7 +2329,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let sil_e1', ie_typ = res_trans_ie.return in Some { empty_control with - instrs= [Sil.Store {e1= var_exp; root_typ= ie_typ; e2= sil_e1'; loc= sil_loc}] } + instrs= + [ Sil.Store + {e1= var_exp; root_typ= ie_typ; typ= ie_typ; e2= sil_e1'; loc= sil_loc} ] } in let pre_init_opt = match var_exp with @@ -2642,7 +2646,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s if List.exists ~f:(Exp.equal ret_exp) res_trans_stmt.control.initd_exps then [] else let sil_expr, _ = res_trans_stmt.return in - [Sil.Store {e1= ret_exp; root_typ= ret_type; e2= sil_expr; loc= sil_loc}] + [ Sil.Store + {e1= ret_exp; root_typ= ret_type; typ= ret_typ; e2= sil_expr; loc= sil_loc} ] in let instrs = var_instrs @ res_trans_stmt.control.instrs @ ret_instrs in let ret_node = mk_ret_node instrs in diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 5446bb097..f402dce52 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -679,7 +679,8 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex let ret_id = Ident.create_fresh Ident.knormal in let call_instr = Sil.Call ((ret_id, return_type), callee_fun, call_args, loc, call_flags) in let set_instr = - Sil.Store {e1= Exp.Lvar sil_var; root_typ= return_type; e2= Exp.Var ret_id; loc} + Sil.Store + {e1= Exp.Lvar sil_var; root_typ= return_type; typ= return_type; e2= Exp.Var ret_id; loc} in instrs @ [call_instr; set_instr] in @@ -869,7 +870,9 @@ let instruction (context : JContext.t) pc instr : translation = | AffectVar (var, expr) -> let stml, sil_expr, sil_type = expression context pc expr in let pvar = JContext.set_pvar context var sil_type in - let sil_instr = Sil.Store {e1= Exp.Lvar pvar; root_typ= sil_type; e2= sil_expr; loc} in + let sil_instr = + Sil.Store {e1= Exp.Lvar pvar; root_typ= sil_type; typ= sil_type; e2= sil_expr; loc} + in let node_kind = Procdesc.Node.Stmt_node MethodBody in let node = create_node node_kind (stml @ [sil_instr]) in Instr node @@ -883,7 +886,8 @@ let instruction (context : JContext.t) pc instr : translation = let stml, sil_expr, _ = expression context pc expr in let sil_instrs = let return_instr = - Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_expr; loc} + Sil.Store + {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_expr; loc} in if return_not_null () then [assume_not_null loc sil_expr; return_instr] else [return_instr] @@ -900,6 +904,7 @@ let instruction (context : JContext.t) pc instr : translation = Sil.Store { e1= Exp.Lindex (sil_expr_array, sil_expr_index) ; root_typ= value_typ + ; typ= value_typ ; e2= sil_expr_value ; loc } in @@ -909,13 +914,14 @@ let instruction (context : JContext.t) pc instr : translation = Instr node | AffectField (e_lhs, cn, fs, e_rhs) -> let stml1, sil_expr_lhs, _ = expression context pc e_lhs in - let stml2, sil_expr_rhs, _ = expression context pc e_rhs in + let stml2, sil_expr_rhs, rhs_typ = expression context pc e_rhs in let field_name = get_field_name program false tenv cn fs in let type_of_the_surrounding_class = JTransType.get_class_type_no_pointer program tenv cn in let type_of_the_root_of_e_lhs = type_of_the_surrounding_class in let expr_off = Exp.Lfield (sil_expr_lhs, field_name, type_of_the_surrounding_class) in let sil_instr = - Sil.Store {e1= expr_off; root_typ= type_of_the_root_of_e_lhs; e2= sil_expr_rhs; loc} + Sil.Store + {e1= expr_off; root_typ= type_of_the_root_of_e_lhs; typ= rhs_typ; e2= sil_expr_rhs; loc} in let node_kind = Procdesc.Node.Stmt_node MethodBody in let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in @@ -927,13 +933,14 @@ let instruction (context : JContext.t) pc instr : translation = Exp.Lvar var_name in let stml1, sil_expr_lhs = ([], class_exp) in - let stml2, sil_expr_rhs, _ = expression context pc e_rhs in + let stml2, sil_expr_rhs, rhs_typ = expression context pc e_rhs in let field_name = get_field_name program true tenv cn fs in let type_of_the_surrounding_class = JTransType.get_class_type_no_pointer program tenv cn in let type_of_the_root_of_e_lhs = type_of_the_surrounding_class in let expr_off = Exp.Lfield (sil_expr_lhs, field_name, type_of_the_surrounding_class) in let sil_instr = - Sil.Store {e1= expr_off; root_typ= type_of_the_root_of_e_lhs; e2= sil_expr_rhs; loc} + Sil.Store + {e1= expr_off; root_typ= type_of_the_root_of_e_lhs; typ= rhs_typ; e2= sil_expr_rhs; loc} in let node_kind = Procdesc.Node.Stmt_node MethodBody in let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in @@ -971,7 +978,9 @@ let instruction (context : JContext.t) pc instr : translation = | Throw expr -> let instrs, sil_expr, _ = expression context pc expr in let sil_exn = Exp.Exn sil_expr in - let sil_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in + let sil_instr = + Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc} + in let node = create_node Procdesc.Node.throw_kind (instrs @ [sil_instr]) in JContext.add_goto_jump context pc JContext.Exit ; Instr node @@ -996,7 +1005,8 @@ let instruction (context : JContext.t) pc instr : translation = in let pvar = JContext.set_pvar context var class_type in let set_instr = - Sil.Store {e1= Exp.Lvar pvar; root_typ= class_type; e2= Exp.Var ret_id; loc} + Sil.Store + {e1= Exp.Lvar pvar; root_typ= class_type; typ= class_type; e2= Exp.Var ret_id; loc} in let instrs = (new_instr :: call_instrs) @ [set_instr] in let node_kind = create_node_kind constr_procname in @@ -1014,7 +1024,12 @@ let instruction (context : JContext.t) pc instr : translation = Sil.Call ((ret_id, array_type), builtin_new_array, call_args, loc, CallFlags.default) in let set_instr = - Sil.Store {e1= Exp.Lvar array_name; root_typ= array_type; e2= Exp.Var ret_id; loc} + Sil.Store + { e1= Exp.Lvar array_name + ; root_typ= array_type + ; typ= array_type + ; e2= Exp.Var ret_id + ; loc } in let node_kind = Procdesc.Node.Stmt_node MethodBody in let node = create_node node_kind (instrs @ [call_instr; set_instr]) in @@ -1121,7 +1136,9 @@ let instruction (context : JContext.t) pc instr : translation = Typ.Procname.Java.Static in let sil_exn = Exp.Exn (Exp.Var ret_id) in - let set_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in + let set_instr = + Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc} + in let npe_instrs = instrs @ [sil_prune_null] @ (new_instr :: call_instrs) @ [set_instr] in create_node npe_kind npe_instrs in @@ -1181,7 +1198,9 @@ let instruction (context : JContext.t) pc instr : translation = [] I_Special Typ.Procname.Java.Static in let sil_exn = Exp.Exn (Exp.Var ret_id) in - let set_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in + let set_instr = + Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc} + in let out_of_bound_instrs = instrs @ [sil_assume_out_of_bound] @ (new_instr :: call_instrs) @ [set_instr] in @@ -1229,7 +1248,9 @@ let instruction (context : JContext.t) pc instr : translation = [] I_Special Typ.Procname.Java.Static in let sil_exn = Exp.Exn (Exp.Var ret_id) in - let set_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in + let set_instr = + Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= sil_exn; loc} + in let cce_instrs = instrs @ [call; asssume_not_instance_of] @ (new_instr :: call_instrs) @ [set_instr] in diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index fc5a94107..404f4186a 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -36,7 +36,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle Sil.Load {id= id_ret_val; e= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; loc} in let instr_deactivate_exn = - Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= Exp.null; loc} + Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; typ= ret_type; e2= Exp.null; loc} in let instr_unwrap_ret_val = let unwrap_builtin = Exp.Const (Const.Cfun BuiltinDecl.__unwrap_exception) in @@ -101,11 +101,20 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle in let instr_set_catch_var = let catch_var = JContext.set_pvar context handler.JBir.e_catch_var ret_type in - Sil.Store {e1= Exp.Lvar catch_var; root_typ= ret_type; e2= Exp.Var id_exn_val; loc} + Sil.Store + { e1= Exp.Lvar catch_var + ; root_typ= ret_type + ; typ= ret_type + ; e2= Exp.Var id_exn_val + ; loc } in let instr_rethrow_exn = Sil.Store - {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= Exp.Exn (Exp.Var id_exn_val); loc} + { e1= Exp.Lvar ret_var + ; root_typ= ret_type + ; typ= ret_type + ; e2= Exp.Exn (Exp.Var id_exn_val) + ; loc } in let node_kind_true = Procdesc.Node.Prune_node (true, if_kind, PruneNodeKind_ExceptionHandler) diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 84b66cd30..0ceb91979 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -85,6 +85,7 @@ let set_transitions loc active_transitions = Sil.Store { e1= ToplUtils.static_var (ToplName.transition i) ; root_typ= ToplUtils.topl_class_typ + ; typ= ToplUtils.topl_class_typ ; e2= value ; loc } in diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml index 36c34b74e..f74977066 100644 --- a/infer/src/topl/ToplMonitor.ml +++ b/infer/src/topl/ToplMonitor.ml @@ -176,7 +176,11 @@ let sil_assign lhs rhs = ; typ= ToplUtils.any_type ; loc= sourcefile_location () } ; Sil.Store - {e1= lhs; root_typ= ToplUtils.any_type; e2= Exp.Var tempvar; loc= sourcefile_location ()} ] + { e1= lhs + ; root_typ= ToplUtils.any_type + ; typ= ToplUtils.any_type + ; e2= Exp.Var tempvar + ; loc= sourcefile_location () } ] let assign lhs rhs : node_generator = stmt_node (sil_assign lhs rhs) @@ -258,6 +262,7 @@ let generate_execute_state automaton proc_name = [ Sil.Store { e1= ToplUtils.static_var ToplName.state ; root_typ= Typ.mk (Tint IInt) + ; typ= Typ.mk (Tint IInt) ; e2= Exp.int (IntLit.of_int transition.target) ; loc= sourcefile_location () } ] :: step (ToplUtils.static_var ToplName.retval) transition.label.ToplAst.return diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 0f285188e..7e138d077 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -73,7 +73,7 @@ module StructuredSil = struct let make_set ~rhs_typ ~lhs_exp ~rhs_exp = - Cmd (Sil.Store {e1= lhs_exp; root_typ= rhs_typ; e2= rhs_exp; loc= dummy_loc}) + Cmd (Sil.Store {e1= lhs_exp; root_typ= rhs_typ; typ= rhs_typ; e2= rhs_exp; loc= dummy_loc}) let make_call ?(procname = dummy_procname) ?return:return_opt args =