Module Pulselib.PulsePathContext

type t = {
  1. conditions : Pulselib.PulseBasicInterface.ValueHistory.t list;
    (*

    Each history represents a conditional that is affecting the path currently, with the most recent conditional first. The idea is to add these histories to the histories of all variables and memory locations modified while under the influence of these conditionals.

    *)
  2. timestamp : Pulselib.PulseBasicInterface.Timestamp.t;
    (*

    step number in an intra-procedural analysis

    *)
}
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
include Ppx_compare_lib.Equal.S with type t := t
val equal : t Base__Ppx_compare_lib.equal
include Absint.AbstractDomain.Disjunct with type t := t
include Absint.AbstractDomain.Comparable with type t := t
include IStdlib.PrettyPrintable.PrintableType with type t := t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool

the implication relation: lhs <= rhs means lhs |- rhs

val equal_fast : t -> t -> bool

equal_fast x y must imply x <=> y; it's a good idea for this function to be "fast", e.g. not depend on the size of its input

val is_normal : t -> bool

test if the abstract state represents exactly concrete states

val is_exceptional : t -> bool

test if the abstract state represents exactly exceptional concrete states

val is_executable : t -> bool

test if the abstract state represents executable states, e.g. ContinueProgram or ExceptionRaised.

val exceptional_to_normal : t -> t

convert all exceptional states into normal states (used when reaching a handler)

val initial : t
val post_exec_instr : t -> t

call this after each step of the symbolic execution to update the path information