Module InferModules.BiabductionSummary

module Jprop : sig ... end

Module for joined props: the result of joining together propositions repeatedly

module Visitedset : InferStdlib.IStd.Caml.Set.S with type Visitedset.elt = InferIR.Procdesc.Node.id * int list

set of visited nodes: node id and list of lines of all the instructions

type 'a spec = {
pre : 'a Jprop.t;
posts : ('a Prop.t * Paths.Path.t) list;
visited : Visitedset.t;
}

A spec consists of: pre: a joined prop posts: a list of props with path visited: a list of pairs (node_id, line) for the visited nodes

module NormSpec : sig ... end

encapsulate type for normalized specs

val normalized_specs_to_specs : NormSpec.t list -> Prop.normal spec list

Cast a list of normalized specs to a list of specs

val pp_spec : Stdlib.Format.formatter -> _ spec -> unit
val spec_normalize : InferIR.Tenv.t -> Prop.normal spec -> NormSpec.t

Convert spec into normal form w.r.t. variable renaming

type phase =
| FOOTPRINT
| RE_EXECUTION
val equal_phase : phase -> phase -> bool
val string_of_phase_short : phase -> string
val get_specs_from_preposts : NormSpec.t list option -> Prop.normal spec list
type t = {
preposts : NormSpec.t list;
phase : phase;
}
val opt_get_phase : t option -> phase
val pp : InferStdlib.Pp.env -> Stdlib.Format.formatter -> t -> unit