Module Absint.AnalysisState

State of symbolic execution

val get_node : unit -> IR.Procdesc.Node.t option

Get last node seen in symbolic execution

val get_remaining_disjuncts : unit -> int option

Get number of remaining disjuncts in the transfer function for Pulse

val set_instr : IR.Sil.instr -> unit

Set last instruction seen in symbolic execution

val set_node : IR.Procdesc.Node.t -> unit

Set last node seen in symbolic execution

val set_remaining_disjuncts : int -> unit

Set number of remaining disjuncts in the transfer function for Pulse

val set_session : int -> unit

Set last session seen in symbolic execution

val reset_active_loops : unit -> unit

Reset the set ot active loops

val is_active_loop : IR.Procdesc.Node.id -> bool

Test if node id is an active loop header

val set_active_loops : IR.Procdesc.IdSet.t -> unit

Declare a set of active loop header

val set_active_loop : IR.Procdesc.Node.id -> unit

Declare an other active loop header