Module `Biabduction.Dom`

Join Operators

val pathset_join : BiabductionSummary.t Absint.InterproceduralAnalysis.t -> Paths.PathSet.t -> Paths.PathSet.t -> Paths.PathSet.t * Paths.PathSet.t: Join two pathsets

val proplist_collapse_pre : IR.Tenv.t -> Prop.normal Prop.t list -> Prop.normal BiabductionSummary.Jprop.t list

Meet Operators

val propset_meet_generate_pre : IR.Tenv.t -> Propset.t -> Prop.normal Prop.t list: propset_meet_generate_pre generates new symbolic heaps (i.e., props) by applying the partial meet operator, adds the generated heaps to the argument propset, and returns the resulting propset. This function is tuned for combining preconditions.