|
|
@ -98,14 +98,14 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
|
|
|
|
Ident.create kind !max_stamp in
|
|
|
|
Ident.create kind !max_stamp in
|
|
|
|
let res =
|
|
|
|
let res =
|
|
|
|
match Tenv.expand_type tenv t, off with
|
|
|
|
match Tenv.expand_type tenv t, off with
|
|
|
|
| Typ.Tstruct _, [] ->
|
|
|
|
| Tstruct _, [] ->
|
|
|
|
([], Sil.Estruct ([], inst), t)
|
|
|
|
([], Sil.Estruct ([], inst), t)
|
|
|
|
| Typ.Tstruct ({ Typ.instance_fields; static_fields } as struct_typ ),
|
|
|
|
| Tstruct ({ fields; statics } as struct_typ ),
|
|
|
|
(Sil.Off_fld (f, _)):: off' ->
|
|
|
|
(Sil.Off_fld (f, _)):: off' ->
|
|
|
|
let _, t', _ =
|
|
|
|
let _, t', _ =
|
|
|
|
try
|
|
|
|
try
|
|
|
|
IList.find (fun (f', _, _) -> Ident.fieldname_equal f f')
|
|
|
|
IList.find (fun (f', _, _) -> Ident.fieldname_equal f f')
|
|
|
|
(instance_fields @ static_fields)
|
|
|
|
(fields @ statics)
|
|
|
|
with Not_found ->
|
|
|
|
with Not_found ->
|
|
|
|
raise (Exceptions.Bad_footprint __POS__) in
|
|
|
|
raise (Exceptions.Bad_footprint __POS__) in
|
|
|
|
let atoms', se', res_t' =
|
|
|
|
let atoms', se', res_t' =
|
|
|
@ -114,9 +114,10 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
|
|
|
|
let se = Sil.Estruct ([(f, se')], inst) in
|
|
|
|
let se = Sil.Estruct ([(f, se')], inst) in
|
|
|
|
let replace_typ_of_f (f', t', a') =
|
|
|
|
let replace_typ_of_f (f', t', a') =
|
|
|
|
if Ident.fieldname_equal f f' then (f, res_t', a') else (f', t', a') in
|
|
|
|
if Ident.fieldname_equal f f' then (f, res_t', a') else (f', t', a') in
|
|
|
|
let instance_fields' =
|
|
|
|
let fields' =
|
|
|
|
IList.sort Typ.fld_typ_ann_compare (IList.map replace_typ_of_f instance_fields) in
|
|
|
|
IList.sort Typ.fld_typ_ann_compare (IList.map replace_typ_of_f fields) in
|
|
|
|
(atoms', se, Typ.Tstruct { struct_typ with Typ.instance_fields = instance_fields'})
|
|
|
|
(atoms', se,
|
|
|
|
|
|
|
|
Typ.Tstruct (Typ.mk_struct ~default:struct_typ ~fields:fields' struct_typ.name))
|
|
|
|
| Typ.Tstruct _, (Sil.Off_index e):: off' ->
|
|
|
|
| Typ.Tstruct _, (Sil.Off_index e):: off' ->
|
|
|
|
let atoms', se', res_t' =
|
|
|
|
let atoms', se', res_t' =
|
|
|
|
create_struct_values
|
|
|
|
create_struct_values
|
|
|
@ -205,12 +206,12 @@ let rec _strexp_extend_values
|
|
|
|
_strexp_extend_values
|
|
|
|
_strexp_extend_values
|
|
|
|
pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
|
|
|
|
pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
|
|
|
|
| (Sil.Off_fld (f, _)):: off', Sil.Estruct (fsel, inst'),
|
|
|
|
| (Sil.Off_fld (f, _)):: off', Sil.Estruct (fsel, inst'),
|
|
|
|
Typ.Tstruct ({ Typ.instance_fields; static_fields } as struct_typ) ->
|
|
|
|
Tstruct ({ fields; statics } as struct_typ) ->
|
|
|
|
let replace_fv new_v fv = if Ident.fieldname_equal (fst fv) f then (f, new_v) else fv in
|
|
|
|
let replace_fv new_v fv = if Ident.fieldname_equal (fst fv) f then (f, new_v) else fv in
|
|
|
|
let _, typ', _ =
|
|
|
|
let _, typ', _ =
|
|
|
|
try
|
|
|
|
try
|
|
|
|
IList.find (fun (f', _, _) -> Ident.fieldname_equal f f')
|
|
|
|
IList.find (fun (f', _, _) -> Ident.fieldname_equal f f')
|
|
|
|
(instance_fields @ static_fields)
|
|
|
|
(fields @ statics)
|
|
|
|
with Not_found ->
|
|
|
|
with Not_found ->
|
|
|
|
raise (Exceptions.Missing_fld (f, __POS__)) in
|
|
|
|
raise (Exceptions.Missing_fld (f, __POS__)) in
|
|
|
|
begin
|
|
|
|
begin
|
|
|
@ -223,10 +224,11 @@ let rec _strexp_extend_values
|
|
|
|
let replace_fse = replace_fv res_se' in
|
|
|
|
let replace_fse = replace_fv res_se' in
|
|
|
|
let res_fsel' = IList.sort Sil.fld_strexp_compare (IList.map replace_fse fsel) in
|
|
|
|
let res_fsel' = IList.sort Sil.fld_strexp_compare (IList.map replace_fse fsel) in
|
|
|
|
let replace_fta (f, t, a) = let f', t' = replace_fv res_typ' (f, t) in (f', t', a) in
|
|
|
|
let replace_fta (f, t, a) = let f', t' = replace_fv res_typ' (f, t) in (f', t', a) in
|
|
|
|
let instance_fields' =
|
|
|
|
let fields' =
|
|
|
|
IList.sort Typ.fld_typ_ann_compare (IList.map replace_fta instance_fields) in
|
|
|
|
IList.sort Typ.fld_typ_ann_compare (IList.map replace_fta fields) in
|
|
|
|
let struct_typ =
|
|
|
|
let struct_typ =
|
|
|
|
Typ.Tstruct { struct_typ with Typ.instance_fields = instance_fields' } in
|
|
|
|
Typ.Tstruct
|
|
|
|
|
|
|
|
(Typ.mk_struct ~default:struct_typ ~fields:fields' struct_typ.name) in
|
|
|
|
(res_atoms', Sil.Estruct (res_fsel', inst'), struct_typ) :: acc in
|
|
|
|
(res_atoms', Sil.Estruct (res_fsel', inst'), struct_typ) :: acc in
|
|
|
|
IList.fold_left replace [] atoms_se_typ_list'
|
|
|
|
IList.fold_left replace [] atoms_se_typ_list'
|
|
|
|
with Not_found ->
|
|
|
|
with Not_found ->
|
|
|
@ -235,9 +237,11 @@ let rec _strexp_extend_values
|
|
|
|
pname tenv orig_prop footprint_part kind max_stamp typ' off' inst in
|
|
|
|
pname tenv orig_prop footprint_part kind max_stamp typ' off' inst in
|
|
|
|
let res_fsel' = IList.sort Sil.fld_strexp_compare ((f, se'):: fsel) in
|
|
|
|
let res_fsel' = IList.sort Sil.fld_strexp_compare ((f, se'):: fsel) in
|
|
|
|
let replace_fta (f', t', a') = if Ident.fieldname_equal f' f then (f, res_typ', a') else (f', t', a') in
|
|
|
|
let replace_fta (f', t', a') = if Ident.fieldname_equal f' f then (f, res_typ', a') else (f', t', a') in
|
|
|
|
let instance_fields' =
|
|
|
|
let fields' =
|
|
|
|
IList.sort Typ.fld_typ_ann_compare (IList.map replace_fta instance_fields) in
|
|
|
|
IList.sort Typ.fld_typ_ann_compare (IList.map replace_fta fields) in
|
|
|
|
let struct_typ = Typ.Tstruct { struct_typ with Typ.instance_fields = instance_fields' } in
|
|
|
|
let struct_typ =
|
|
|
|
|
|
|
|
Typ.Tstruct
|
|
|
|
|
|
|
|
(Typ.mk_struct ~default:struct_typ ~fields:fields' struct_typ.name) in
|
|
|
|
[(atoms', Sil.Estruct (res_fsel', inst'), struct_typ)]
|
|
|
|
[(atoms', Sil.Estruct (res_fsel', inst'), struct_typ)]
|
|
|
|
end
|
|
|
|
end
|
|
|
|
| (Sil.Off_fld (_, _)):: _, _, _ ->
|
|
|
|
| (Sil.Off_fld (_, _)):: _, _, _ ->
|
|
|
@ -1031,11 +1035,11 @@ let type_at_offset tenv texp off =
|
|
|
|
let rec strip_offset off typ =
|
|
|
|
let rec strip_offset off typ =
|
|
|
|
match off, Tenv.expand_type tenv typ with
|
|
|
|
match off, Tenv.expand_type tenv typ with
|
|
|
|
| [], _ -> Some typ
|
|
|
|
| [], _ -> Some typ
|
|
|
|
| (Sil.Off_fld (f, _)):: off', Typ.Tstruct { Typ.instance_fields } ->
|
|
|
|
| (Sil.Off_fld (f, _)):: off', Tstruct { fields } ->
|
|
|
|
(try
|
|
|
|
(try
|
|
|
|
let typ' =
|
|
|
|
let typ' =
|
|
|
|
(fun (_, y, _) -> y)
|
|
|
|
(fun (_, y, _) -> y)
|
|
|
|
(IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') instance_fields) in
|
|
|
|
(IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') fields) in
|
|
|
|
strip_offset off' typ'
|
|
|
|
strip_offset off' typ'
|
|
|
|
with Not_found -> None)
|
|
|
|
with Not_found -> None)
|
|
|
|
| (Sil.Off_index _) :: off', Typ.Tarray (typ', _) ->
|
|
|
|
| (Sil.Off_index _) :: off', Typ.Tarray (typ', _) ->
|
|
|
|