@ -148,10 +148,10 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
( Sil . Aeq ( e , e' ) :: atoms' , se , res_t )
| Sil . Off_fld _ :: _ ->
assert false )
| Tint _ , [] | Tfloat _ , [] | Tvoid , [] | Tfun _ , [] | Tptr _ , [] | TVar _ , [] ->
| Tint _ , [] | Tfloat _ , [] | Tvoid , [] | Tfun , [] | Tptr _ , [] | TVar _ , [] ->
let id = new_id () in
( [] , Sil . Eexp ( Exp . Var id , inst ) , t )
| ( Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _ | TVar _ ) , Off_index e :: off' ->
| ( Tint _ | Tfloat _ | Tvoid | Tfun | Tptr _ | TVar _ ) , Off_index e :: off' ->
(* In this case, we lift t to the t array. *)
let t' , mk_typ_f =
match t . Typ . desc with
@ -168,7 +168,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
let se = Sil . Earray ( len , [ ( e' , se' ) ] , inst ) in
let res_t = mk_typ_f ( Tarray { elt = res_t' ; length = None ; stride = None } ) in
( Sil . Aeq ( e , e' ) :: atoms' , se , res_t )
| Tint _ , _ | Tfloat _ , _ | Tvoid , _ | Tfun _ , _ | Tptr _ , _ | TVar _ , _ ->
| Tint _ , _ | Tfloat _ , _ | Tvoid , _ | Tfun , _ | Tptr _ , _ | TVar _ , _ ->
fail t off _ _ POS__
in
if Config . trace_rearrange then (
@ -248,7 +248,7 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
raise ( Exceptions . Missing_fld ( f , _ _ POS__ ) ) )
| Off_fld _ :: _ , _ , _ ->
raise ( Exceptions . Bad_footprint _ _ POS__ )
| Off_index _ :: _ , Sil . Eexp _ , ( Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _ )
| Off_index _ :: _ , Sil . Eexp _ , ( Tint _ | Tfloat _ | Tvoid | Tfun | Tptr _ )
| Off_index _ :: _ , Sil . Estruct _ , Tstruct _ ->
(* L.d_strln ~color:Orange "turn into an array"; *)
let len =
@ -456,14 +456,14 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst :
in
let create_ptsto footprint_part off0 =
match ( root , off0 , typ . Typ . desc ) with
| Exp . Lvar pvar , [] , Typ . Tfun _ ->
| Exp . Lvar pvar , [] , Typ . Tfun ->
let fun_name = Typ . Procname . from_string_c_fun ( Mangled . to_string ( Pvar . get_name pvar ) ) in
let fun_exp = Exp . Const ( Const . Cfun fun_name ) in
( []
, Prop . mk_ptsto tenv root
( Sil . Eexp ( fun_exp , inst ) )
( Exp . Sizeof { typ ; nbytes = None ; dynamic_length = None ; subtype } ) )
| _ , [] , Typ . Tfun _ ->
| _ , [] , Typ . Tfun ->
let atoms , se , typ =
create_struct_values pname tenv orig_prop footprint_part Ident . kfootprint max_stamp typ
off0 inst