@ -99,7 +99,7 @@ let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para: Sil.hpara) =
let ( para_fst_start , para_fst_rest ) =
let ( para_fst_start , para_fst_rest ) =
let mark_impl_flag hpred = { Match . hpred = hpred ; Match . flag = impl_ok1 } in
let mark_impl_flag hpred = { Match . hpred = hpred ; Match . flag = impl_ok1 } in
match para_fst with
match para_fst with
| [] -> failwithf " mk_rule_ptspts_ls (Empty Para): %a " ( Sil . pp_hpara Pp . text ) para
| [] -> L . out " @.@.ERROR (Empty Para): %a @.@. " ( Sil . pp_hpara Pp . text ) para ; assert false
| hpred :: hpreds ->
| hpred :: hpreds ->
let hpat = mark_impl_flag hpred in
let hpat = mark_impl_flag hpred in
let hpats = List . map ~ f : mark_impl_flag hpreds in
let hpats = List . map ~ f : mark_impl_flag hpreds in
@ -128,7 +128,7 @@ let mk_rule_ptsls_ls tenv k2 impl_ok1 impl_ok2 para =
let ( ids_exist , para_inst ) = Sil . hpara_instantiate para exp_base exp_next exps_shared in
let ( ids_exist , para_inst ) = Sil . hpara_instantiate para exp_base exp_next exps_shared in
let ( para_inst_start , para_inst_rest ) =
let ( para_inst_start , para_inst_rest ) =
match para_inst with
match para_inst with
| [] -> failwithf " mk_rule_ptsls_ls (Empty Para): %a " ( Sil . pp_hpara Pp . text ) para
| [] -> L . out " @.@.ERROR (Empty Para): %a @.@. " ( Sil . pp_hpara Pp . text ) para ; assert false
| hpred :: hpreds ->
| hpred :: hpreds ->
let allow_impl hpred = { Match . hpred = hpred ; Match . flag = impl_ok1 } in
let allow_impl hpred = { Match . hpred = hpred ; Match . flag = impl_ok1 } in
( allow_impl hpred , List . map ~ f : allow_impl hpreds ) in
( allow_impl hpred , List . map ~ f : allow_impl hpreds ) in
@ -252,7 +252,7 @@ let mk_rule_ptspts_dll tenv impl_ok1 impl_ok2 para =
let ( para_fst_start , para_fst_rest ) =
let ( para_fst_start , para_fst_rest ) =
let mark_impl_flag hpred = { Match . hpred = hpred ; Match . flag = impl_ok1 } in
let mark_impl_flag hpred = { Match . hpred = hpred ; Match . flag = impl_ok1 } in
match para_fst with
match para_fst with
| [] -> failwithf " mk_rule_ptspts_dll (Empty DLL para): %a " ( Sil . pp_hpara_dll Pp . text ) para
| [] -> L . out " @.@.ERROR (Empty DLL para): %a@.@. " ( Sil . pp_hpara_dll Pp . text ) para ; assert false
| hpred :: hpreds ->
| hpred :: hpreds ->
let hpat = mark_impl_flag hpred in
let hpat = mark_impl_flag hpred in
let hpats = List . map ~ f : mark_impl_flag hpreds in
let hpats = List . map ~ f : mark_impl_flag hpreds in
@ -430,7 +430,8 @@ let typ_get_recursive_flds tenv typ_exp =
| Exp . Var _ -> [] (* type of |-> not known yet *)
| Exp . Var _ -> [] (* type of |-> not known yet *)
| Exp . Const _ -> []
| Exp . Const _ -> []
| _ ->
| _ ->
failwithf " @.typ_get_recursive: unexpected type expr: %a@. " Exp . pp typ_exp
L . out " @.typ_get_recursive: unexpected type expr: %a@. " Exp . pp typ_exp ;
assert false
let discover_para_roots tenv p root1 next1 root2 next2 : Sil . hpara option =
let discover_para_roots tenv p root1 next1 root2 next2 : Sil . hpara option =
let eq_arg1 = Exp . equal root1 next1 in
let eq_arg1 = Exp . equal root1 next1 in
@ -601,7 +602,7 @@ let eqs_solve ids_in eqs_in =
if not ( List . exists ~ f : ( fun id' -> Ident . equal id id' ) ids_in ) then None
if not ( List . exists ~ f : ( fun id' -> Ident . equal id id' ) ids_in ) then None
else
else
let sub' = match Sil . extend_sub sub id e with
let sub' = match Sil . extend_sub sub id e with
| None -> failwithf " ERROR : Buggy Implementation "
| None -> L . out " @.@.ERROR : Buggy Implementation.@.@. " ; assert false
| Some sub' -> sub' in
| Some sub' -> sub' in
let eqs_rest' = eqs_sub sub' eqs_rest in
let eqs_rest' = eqs_sub sub' eqs_rest in
solve sub' eqs_rest' in
solve sub' eqs_rest' in