Biabduction.Rearrange
Re-arrangement and extension of structures with fresh variables
val is_only_pt_by_fld_or_param_nonnull :
IR.Procdesc.t ->
IR.Tenv.t ->
Prop.normal Prop.t ->
IR.Exp.t ->
bool
val check_dereference_error :
IR.Tenv.t ->
IR.Procdesc.t ->
Prop.normal Prop.t ->
IR.Exp.t ->
IBase.Location.t ->
unit
Check for dereference errors: dereferencing 0, a freed value, or an undefined value
val rearrange :
?report_deref_errors:bool ->
BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
IR.Exp.t ->
IR.Typ.t ->
Prop.normal Prop.t ->
IBase.Location.t ->
Predicates.offset list Prop.prop_iter list
rearrange lexp prop
rearranges prop
into the form prop' * lexp|->strexp:typ
. It returns an iterator with lexp |-> strexp: typ
as current predicate and the path (an offsetlist
) which leads to lexp
as the iterator state.