@ -1415,7 +1415,11 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
| _ , Sil . Tstruct _ -> (* the struct type of fld is known *)
| _ , Sil . Tstruct _ -> (* the struct type of fld is known *)
Sil . Sizeof ( typ_fld , Sil . Subtype . exact )
Sil . Sizeof ( typ_fld , Sil . Subtype . exact )
| Sil . Sizeof ( _ t , st ) , _ -> (* the struct type of fld is not known -- typically Tvoid *)
| Sil . Sizeof ( _ t , st ) , _ -> (* the struct type of fld is not known -- typically Tvoid *)
Sil . Sizeof ( Sil . Tstruct ( [ ( fld , _ t , Sil . item_annotation_empty ) ] , [] , Sil . Struct , None , [] , [] , Sil . item_annotation_empty ) , st ) (* None as we don't know the stuct name *)
Sil . Sizeof
( Sil . Tstruct
( [ ( fld , _ t , Sil . item_annotation_empty ) ] ,
[] , Csu . Struct , None , [] , [] , Sil . item_annotation_empty ) , st )
(* None as we don't know the stuct name *)
| _ -> raise ( Failure " expand_hpred_pointer: Unexpected non-sizeof type in Lfield " ) in
| _ -> raise ( Failure " expand_hpred_pointer: Unexpected non-sizeof type in Lfield " ) in
let hpred' = Sil . Hpointsto ( e , Sil . Estruct ( [ ( fld , se ) ] , Sil . inst_none ) , t' ) in
let hpred' = Sil . Hpointsto ( e , Sil . Estruct ( [ ( fld , se ) ] , Sil . inst_none ) , t' ) in
expand true true hpred'
expand true true hpred'
@ -1443,8 +1447,8 @@ let serializable_type = Mangled.from_string "java.io.Serializable"
let cloneable_type = Mangled . from_string " java.lang.Cloneable "
let cloneable_type = Mangled . from_string " java.lang.Cloneable "
let is_interface tenv c =
let is_interface tenv c =
match Sil . tenv_lookup tenv ( Sil . TN_csu ( Sil . Class , c ) ) with
match Sil . tenv_lookup tenv ( Sil . TN_csu ( Csu . Class , c ) ) with
| Some ( Sil . Tstruct ( fields , sfields , Sil . Class , Some c1' , supers1 , methods , iann ) ) ->
| Some ( Sil . Tstruct ( fields , sfields , Csu . Class , Some c1' , supers1 , methods , iann ) ) ->
( IList . length fields = 0 ) && ( IList . length methods = 0 )
( IList . length fields = 0 ) && ( IList . length methods = 0 )
| _ -> false
| _ -> false
@ -1452,11 +1456,11 @@ let is_interface tenv c =
let check_subclass_tenv tenv c1 c2 =
let check_subclass_tenv tenv c1 c2 =
let rec check ( _ , c ) =
let rec check ( _ , c ) =
Mangled . equal c c2 | | ( Mangled . equal c2 object_type ) | |
Mangled . equal c c2 | | ( Mangled . equal c2 object_type ) | |
match Sil . tenv_lookup tenv ( Sil . TN_csu ( Sil . Class , c ) ) with
match Sil . tenv_lookup tenv ( Sil . TN_csu ( Csu . Class , c ) ) with
| Some ( Sil . Tstruct ( _ , _ , Sil . Class , Some c1' , supers1 , _ , _ ) ) ->
| Some ( Sil . Tstruct ( _ , _ , Csu . Class , Some c1' , supers1 , _ , _ ) ) ->
IList . exists check supers1
IList . exists check supers1
| _ -> false in
| _ -> false in
( check ( Sil . Class , c1 ) )
( check ( Csu . Class , c1 ) )
let check_subclass tenv c1 c2 =
let check_subclass tenv c1 c2 =
let f = check_subclass_tenv tenv in
let f = check_subclass_tenv tenv in
@ -1474,7 +1478,8 @@ let check_subtype_basic_type t1 t2 =
(* * check if t1 is a subtype of t2 *)
(* * check if t1 is a subtype of t2 *)
let rec check_subtype tenv t1 t2 =
let rec check_subtype tenv t1 t2 =
match t1 , t2 with
match t1 , t2 with
| Sil . Tstruct ( _ , _ , Sil . Class , Some c1 , _ , _ , _ ) , Sil . Tstruct ( _ , _ , Sil . Class , Some c2 , _ , _ , _ ) ->
| Sil . Tstruct ( _ , _ , Csu . Class , Some c1 , _ , _ , _ ) ,
Sil . Tstruct ( _ , _ , Csu . Class , Some c2 , _ , _ , _ ) ->
( check_subclass tenv c1 c2 )
( check_subclass tenv c1 c2 )
| Sil . Tarray ( dom_type1 , _ ) , Sil . Tarray ( dom_type2 , _ ) ->
| Sil . Tarray ( dom_type1 , _ ) , Sil . Tarray ( dom_type2 , _ ) ->
@ -1483,14 +1488,15 @@ let rec check_subtype tenv t1 t2 =
| Sil . Tptr ( dom_type1 , _ ) , Sil . Tptr ( dom_type2 , _ ) ->
| Sil . Tptr ( dom_type1 , _ ) , Sil . Tptr ( dom_type2 , _ ) ->
check_subtype tenv dom_type1 dom_type2
check_subtype tenv dom_type1 dom_type2
| Sil . Tarray _ , Sil . Tstruct ( _ , _ , Sil . Class , Some c2 , _ , _ , _ ) ->
| Sil . Tarray _ , Sil . Tstruct ( _ , _ , Csu . Class , Some c2 , _ , _ , _ ) ->
( Mangled . equal c2 serializable_type ) | | ( Mangled . equal c2 cloneable_type ) | | ( Mangled . equal c2 object_type )
( Mangled . equal c2 serializable_type ) | | ( Mangled . equal c2 cloneable_type ) | | ( Mangled . equal c2 object_type )
| _ -> ( check_subtype_basic_type t1 t2 )
| _ -> ( check_subtype_basic_type t1 t2 )
let rec case_analysis_type tenv ( t1 , st1 ) ( t2 , st2 ) =
let rec case_analysis_type tenv ( t1 , st1 ) ( t2 , st2 ) =
match t1 , t2 with
match t1 , t2 with
| Sil . Tstruct ( _ , _ , Sil . Class , Some c1 , _ , _ , _ ) , Sil . Tstruct ( _ , _ , Sil . Class , Some c2 , _ , _ , _ ) ->
| Sil . Tstruct ( _ , _ , Csu . Class , Some c1 , _ , _ , _ ) ,
Sil . Tstruct ( _ , _ , Csu . Class , Some c2 , _ , _ , _ ) ->
( Sil . Subtype . case_analysis ( c1 , st1 ) ( c2 , st2 ) ( check_subclass tenv ) ( is_interface tenv ) )
( Sil . Subtype . case_analysis ( c1 , st1 ) ( c2 , st2 ) ( check_subclass tenv ) ( is_interface tenv ) )
| Sil . Tarray ( dom_type1 , _ ) , Sil . Tarray ( dom_type2 , _ ) ->
| Sil . Tarray ( dom_type1 , _ ) , Sil . Tarray ( dom_type2 , _ ) ->
@ -1499,7 +1505,7 @@ let rec case_analysis_type tenv (t1, st1) (t2, st2) =
| Sil . Tptr ( dom_type1 , _ ) , Sil . Tptr ( dom_type2 , _ ) ->
| Sil . Tptr ( dom_type1 , _ ) , Sil . Tptr ( dom_type2 , _ ) ->
( case_analysis_type tenv ( dom_type1 , st1 ) ( dom_type2 , st2 ) )
( case_analysis_type tenv ( dom_type1 , st1 ) ( dom_type2 , st2 ) )
| Sil . Tstruct ( _ , _ , Sil . Class , Some c1 , _ , _ , _ ) , Sil . Tarray _ ->
| Sil . Tstruct ( _ , _ , Csu . Class , Some c1 , _ , _ , _ ) , Sil . Tarray _ ->
if ( ( Mangled . equal c1 serializable_type ) | | ( Mangled . equal c1 cloneable_type ) | | ( Mangled . equal c1 object_type ) ) &&
if ( ( Mangled . equal c1 serializable_type ) | | ( Mangled . equal c1 cloneable_type ) | | ( Mangled . equal c1 object_type ) ) &&
( st1 < > Sil . Subtype . exact ) then ( Some st1 , None )
( st1 < > Sil . Subtype . exact ) then ( Some st1 , None )
else ( None , Some st1 )
else ( None , Some st1 )
@ -1845,7 +1851,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
match ! Config . curr_language with
match ! Config . curr_language with
| Config . C_CPP -> Sil . Sizeof ( Sil . Tarray ( Sil . Tint Sil . IChar , size ) , Sil . Subtype . exact )
| Config . C_CPP -> Sil . Sizeof ( Sil . Tarray ( Sil . Tint Sil . IChar , size ) , Sil . Subtype . exact )
| Config . Java ->
| Config . Java ->
let object_type = Sil . TN_csu ( Sil . Class , Mangled . from_string " java.lang.String " ) in
let object_type =
Sil . TN_csu ( Csu . Class , Mangled . from_string " java.lang.String " ) in
let typ = match Sil . tenv_lookup tenv object_type with
let typ = match Sil . tenv_lookup tenv object_type with
| Some typ -> typ
| Some typ -> typ
| None -> assert false in
| None -> assert false in
@ -1856,7 +1863,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
let sexp = (* TODO: add appropriate fields *)
let sexp = (* TODO: add appropriate fields *)
Sil . Estruct ( [ ( Ident . create_fieldname ( Mangled . from_string " java.lang.Class.name " ) 0 , Sil . Eexp ( ( Sil . Const ( Sil . Cstr s ) , Sil . Inone ) ) ) ] , Sil . inst_none ) in
Sil . Estruct ( [ ( Ident . create_fieldname ( Mangled . from_string " java.lang.Class.name " ) 0 , Sil . Eexp ( ( Sil . Const ( Sil . Cstr s ) , Sil . Inone ) ) ) ] , Sil . inst_none ) in
let class_texp =
let class_texp =
let class_type = Sil . TN_csu ( Sil . Class , Mangled . from_string " java.lang.Class " ) in
let class_type = Sil . TN_csu ( Csu . Class , Mangled . from_string " java.lang.Class " ) in
let typ = match Sil . tenv_lookup tenv class_type with
let typ = match Sil . tenv_lookup tenv class_type with
| Some typ -> typ
| Some typ -> typ
| None -> assert false in
| None -> assert false in