Module Pulselib.PulseTopl

module BaseDomain = PulseBaseDomain
type static_type = IR.Typ.t
type value_and_type = value * static_type
type event =
  1. | ArrayWrite of {
    1. aw_array : value;
    2. aw_index : value;
    }
  2. | Call of {
    1. return : value_and_type option;
    2. arguments : value_and_type list;
    3. procname : IR.Procname.t;
    }
type state
val compare_state : state -> state -> int
val equal_state : state -> state -> bool
type pulse_state = {
  1. pulse_post : BaseDomain.t;
  2. pulse_pre : BaseDomain.t;
  3. path_condition : Pulselib.PulseBasicInterface.Formula.t;
  4. get_reachable : unit -> Pulselib.PulseBasicInterface.AbstractValue.Set.t;
}

This is a subset of AbductiveDomain.t, which is needed to evolve the topl state. The purpose of this type is to avoid a cyclic dependency between PulseTopl and PulseAbductiveDomain, so that we can keep them separate. The problem is as follows. A PulseAbductiveDomain.t has a PulseTopl.state as a component. Evolving a PulseAbductiveDomain.t must (a) evolve the non-topl parts without looking at the topl parts, which is why PulseTopl.state is abstract, and (b) trigger the evolution of the topl parts, which *should* look at the non-topl parts of the abductive domain. Those necessary non-topl parts are what PulseTopl.pulse_state contains.

val start : unit -> state

Return the initial state of Topl.automaton ().

val small_step : IR.Tenv.t -> IBase.Location.t -> pulse_state -> event -> state -> state
val large_step : call_location:IBase.Location.t -> callee_proc_name:IR.Procname.t -> substitution: (value * Pulselib.PulseBasicInterface.ValueHistory.t) Pulselib.PulseBasicInterface.AbstractValue.Map.t -> pulse_state -> callee_summary:state -> callee_is_manifest:bool -> state -> state

large_step ~call_location ~callee_proc_name ~substitution pulse_state ~callee_summary ~callee_is_manifest state updates state according to callee_summary. The abstract values in pulse_state and state are in one scope, and those in callee_summary in another scope: the substitution maps from the callee scope to the caller scope.

val filter_for_summary : pulse_state -> state -> state

Remove from state those parts that are inconsistent with the path condition. (We do a cheap check to not introduce inconsistent Topl states, but they may become inconsistent because the program path condition is updated later.)

val simplify : pulse_state -> state -> state

Keep only a subset of abstract values. This is used for extracting summaries.

val report_errors : IR.Procdesc.t -> Absint.Errlog.t -> pulse_is_manifest:bool -> state -> unit

Calls Reporting.log_issue with error traces, if any.

val pp_state : Stdlib.Format.formatter -> state -> unit
module Debug : sig ... end