Module Pulselib__PulseTopl

type value = Pulselib.PulseAbstractValue.t
type event =
| ArrayWrite of {
aw_array : value;
aw_index : value;
}
| Call of {
return : value option;
arguments : value list;
procname : IR.Procname.t;
}
type state
val compare_state : state -> state -> int
val equal_state : state -> state -> bool
val start : unit -> state

Return the initial state of Topl.automaton ().

val small_step : IBase.Location.t -> Pulselib.PulsePathCondition.t -> event -> state -> state
val large_step : call_location:IBase.Location.t -> callee_proc_name:IR.Procname.t -> substitution:(value * Pulselib.PulseValueHistory.t) Pulselib.PulseAbstractValue.Map.t -> condition:Pulselib.PulsePathCondition.t -> callee_prepost:state -> state -> state

large_step ~substitution ~condition state ~callee_prepost updates state according to callee_prepost. The abstract values in condition and state are in one scope, and those in callee_prepost in another scope: the substitution maps from the callee scope to the condition&state scope.

val filter_for_summary : Pulselib.PulsePathCondition.t -> 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 mey become inconsistent because the program path condition is updated later.)

val simplify : keep:Pulselib.PulseAbstractValue.Set.t -> state -> state

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

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

Calls Reporting.log_issue with error traces, if any.

val pp_state : Stdlib.Format.formatter -> state -> unit