Module Biabduction.Rearrange

Re-arrangement and extension of structures with fresh variables

exception ARRAY_ACCESS
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

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.