Biabduction.AbsImplementation of Abstraction Functions
val abstract :
BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
Prop.normal Prop.t ->
Prop.normal Prop.tAbstract a proposition.
val abstract_spec :
BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
Prop.normal BiabductionSummary.spec ->
BiabductionSummary.NormSpec.tNormalizes names and applies simplifications, soem of which require looking at both pre and post.
val abstract_junk :
BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
Prop.normal Prop.t ->
Prop.normal Prop.tCheck whether the prop contains junk. If it does, and Config.allowleak is true, remove the junk, otherwise raise a Leak exception.
val abstract_no_symop :
BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
Prop.normal Prop.t ->
Prop.normal Prop.tAbstract a proposition but don't pay a SymOp
val lifted_abstract :
BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
Propset.t ->
Propset.tAbstract each proposition in propset
val remove_redundant_array_elements :
BiabductionSummary.t Absint.InterproceduralAnalysis.t ->
Prop.normal Prop.t ->
Prop.normal Prop.tRemove redundant elements in an array, and check for junk afterwards