diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 794fcbe5f..a379b602a 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -107,8 +107,10 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp | Sil.Tstruct (ftal, sftal, csu, nameo, supers, def_mthds, iann), (Sil.Off_fld (f, _)):: off' -> let _, t', _ = - try IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') ftal - with Not_found -> raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) in + try + IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') (ftal @ sftal) + with Not_found -> + raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) in let atoms', se', res_t' = create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst in @@ -200,9 +202,11 @@ let rec _strexp_extend_values | (Sil.Off_fld (f, _)):: off', Sil.Estruct (fsel, inst'), Sil.Tstruct (ftal, sftal, csu, nameo, supers, def_mthds, iann) -> let replace_fv new_v fv = if Ident.fieldname_equal (fst fv) f then (f, new_v) else fv in - let typ' = - try (fun (x, y, z) -> y) (IList.find (fun (f', t', a') -> Ident.fieldname_equal f f') ftal) - with Not_found -> raise (Exceptions.Missing_fld (f, try assert false with Assert_failure x -> x)) in + let _, typ', _ = + try + IList.find (fun (f', t', a') -> Ident.fieldname_equal f f') (ftal @ sftal) + with Not_found -> + raise (Exceptions.Missing_fld (f, try assert false with Assert_failure x -> x)) in begin try let _, se' = IList.find (fun (f', _) -> Ident.fieldname_equal f f') fsel in diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index c704ecfd0..588950358 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -44,7 +44,7 @@ let rec unroll_type tenv typ off = unroll_type tenv typ' off | Sil.Tstruct (ftal, sftal, _, _, _, _, _), Sil.Off_fld (fld, _) -> begin - try fldlist_assoc fld ftal + try fldlist_assoc fld (ftal @ sftal) with Not_found -> L.d_strln ".... Invalid Field Access ...."; L.d_strln ("Fld : " ^ Ident.fieldname_to_string fld); diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index c348325e6..ef0252673 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -507,10 +507,7 @@ let rec expression context pc expr = | JBir.Field (ex, cn, fs) -> let (idl, instrs, sil_expr) = expression context pc ex in let field_name = get_field_name program false tenv cn fs context in - let sil_type = - try - JTransType.get_class_type_no_pointer program tenv cn - with Frontend_error msg -> assert false in + let sil_type = JTransType.get_class_type_no_pointer program tenv cn in let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in let tmp_id = Ident.create_fresh Ident.knormal in let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in @@ -522,13 +519,7 @@ let rec expression context pc expr = Sil.Lvar var_name in let (idl, instrs, sil_expr) = [], [], class_exp in let field_name = get_field_name program true tenv cn fs context in - let sil_type = - try - match JTransType.get_class_type_no_pointer program tenv cn with - | Sil.Tstruct (ftal, sftal, csu, nameo, supers, def_mthds, iann) -> - Sil.Tstruct (sftal, sftal, csu, nameo, supers, def_mthds, iann) - | t -> t - with Frontend_error msg -> assert false in + let sil_type = JTransType.get_class_type_no_pointer program tenv cn in if JTransStaticField.is_static_final_field context cn fs && use_static_final_fields context then (* when accessing a static final field, we call the initialiser method. *) @@ -874,11 +865,7 @@ let rec instruction context pc instr : translation = let (idl1, stml1, sil_expr_lhs) = [], [], class_exp in let (idl2, stml2, sil_expr_rhs) = expression context pc e_rhs in let field_name = get_field_name program true tenv cn fs context in - let type_of_the_surrounding_class = - match JTransType.get_class_type_no_pointer program tenv cn with - | Sil.Tstruct (ftal, sftal, csu, nameo, supers, def_mthds, iann) -> - Sil.Tstruct (sftal, sftal, csu, nameo, supers, def_mthds, iann) - | t -> t 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 = Sil.Lfield(sil_expr_lhs, field_name, type_of_the_surrounding_class) in let sil_instr = Sil.Set (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in