Pulselib.PulseValueHistory
module CallEvent = PulseCallEvent
module TaintItem = PulseTaintItem
module Timestamp = PulseTimestamp
module CellId : sig ... end
Used to identify which cells (places in the memory) in the current precondition are mentioned in a value history in the current abstract state, i.e. were used to compute that value.
type event =
| Allocation of {
f : CallEvent.t;
location : IBase.Location.t;
timestamp : Timestamp.t;
}
| Assignment of IBase.Location.t * Timestamp.t
| Call of {
f : CallEvent.t;
location : IBase.Location.t;
in_call : t;
timestamp : Timestamp.t;
}
| Capture of {
captured_as : IR.Pvar.t;
mode : IR.CapturedVar.capture_mode;
location : IBase.Location.t;
timestamp : Timestamp.t;
}
| ConditionPassed of {
if_kind : IR.Sil.if_kind;
is_then_branch : bool;
location : IBase.Location.t;
timestamp : Timestamp.t;
}
| CppTemporaryCreated of IBase.Location.t * Timestamp.t
| FormalDeclared of IR.Pvar.t * IBase.Location.t * Timestamp.t
| Invalidated of PulseInvalidation.t * IBase.Location.t * Timestamp.t
| NilMessaging of IBase.Location.t * Timestamp.t
| Returned of IBase.Location.t * Timestamp.t
| StructFieldAddressCreated of IR.Fieldname.t IStdlib.RevList.t
* IBase.Location.t
* Timestamp.t
| TaintSource of TaintItem.t * IBase.Location.t * Timestamp.t
| TaintPropagated of IBase.Location.t * Timestamp.t
| VariableAccessed of IR.Pvar.t * IBase.Location.t * Timestamp.t
| VariableDeclared of IR.Pvar.t * IBase.Location.t * Timestamp.t
and t = private
| Epoch
start of time
*)| Sequence of event * t
Sequence [event, hist]
represents an event event
occurring *after* hist
. Invariant: the timestamp of event
is greater than all the (local, i.e. not inside function calls) timestamps in hist
.
| BinaryOp of IR.Binop.t * t * t
branch history due to a binop
*)| FromCellIds of CellId.Set.t * t
the set of cells that this were used in this history; used in particular in summary application to know which caller value histories should be pre-pended to a callee value history
*)| Multiplex of t list
interlace multiple histories together
*)| UnknownCall of {
f : CallEvent.t;
actuals : t list;
location : IBase.Location.t;
timestamp : Timestamp.t;
}
val yojson_of_event : event -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val epoch : t
val binary_op : IR.Binop.t -> t -> t -> t
val unknown_call :
CallEvent.t ->
t list ->
IBase.Location.t ->
Timestamp.t ->
t
val pp : F.formatter -> t -> unit
val pp_fields : F.formatter -> IR.Fieldname.t IStdlib.RevList.t -> unit
val get_cell_ids : t -> CellId.Set.t option
same as get_cell_ids
but assumes the resulting set is a singleton
multiplex of the histories corresponding to the given cell ids according to the cell id map provided; None
if there are no such histories to multiplex together
type iter_event =
| EnterCall of CallEvent.t * IBase.Location.t
| ReturnFromCall of CallEvent.t * IBase.Location.t
| Event of event
val rev_iter : t -> f:(iter_event -> unit) -> unit
iterate on all events in reverse timestamp order, recursing into the histories inside call events. Timestamp order is the lexicographic order induced by projecting events onto their timestamps and appending timestamps within calls, e.g. the timestamp of the inner assignement in
Call {timestamp=10; in_call=[..., Call{timestamp=4;
in_call=[..., Assignement (...,timestamp=3) ] } ] }
can be written 10.4.3
and the order is such that, e.g., 10.4.3 < 10.5
, 10.5
being the timestamp of the event following the inner Call
event in the example above.
val iter : t -> f:(iter_event -> unit) -> unit
like rev_iter
but iterates in order (by reversing the order iteration)
val location_of_event : event -> IBase.Location.t
val timestamp_of_event : event -> Timestamp.t
val add_to_errlog :
?include_taint_events:bool ->
nesting:int ->
t ->
Absint.Errlog.loc_trace_elem list ->
Absint.Errlog.loc_trace_elem list