Make (infer.Pulselib.PulseCanonValue.Make)

Parameters

module AbductiveDomain : sig ... end

Signature

type t = private Pulselib.PulseBasicInterface.AbstractValue.t

an abstract value that is the canonical representative of its equivalence class (of other abstract values that are equal to it) in the current state (this may not be true if more equalities are added or generally any time the formula inside the state changes)

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

val pp : F.formatter -> t -> unit

module Set : IStdlib.PrettyPrintable.PPSet with type elt = t

val downcast_set : Set.t -> Pulselib.PulseBasicInterface.AbstractValue.Set.t

val unsafe_cast_set : Pulselib.PulseBasicInterface.AbstractValue.Set.t -> Set.t

deprecated unsafe, obviously; please add a comment why you need to use this and suppress this warning locally with [@alert "-deprecated"]

type needs_canon

an abstract value that needs to be normalized; just AbstractValue.t under the hood too

type astate = AbductiveDomain.astate

PulseAbductiveDomain.t but we cannot mention it there otherwise it would create a circular dependency.

Functions to normalize abstract values

Also provided are helper functions that normalize inside of more complex values such as tuples. In that case the functions take care to preserve physical equality if the input value is already its own canonical representative.

We need separate functions for AbstractValue.t and needs_canon values because of the type system. By convention functions that end in ' are the same as the non-primed ones but operate on AbstractValue.t instead of needs_canon ones.

val canon : astate -> needs_canon -> t

fetch the canonical representative of the given needs_canon

val canon' : astate -> Pulselib.PulseBasicInterface.AbstractValue.t -> t

fetch the canonical representative of the given AbstractValue.t

val canon_fst : astate -> (needs_canon * 'a) -> t * 'a

val canon_fst' : 
  astate ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * 'a) ->
  t * 'a

val canon_snd_fst : astate -> ('a * (needs_canon * 'b)) -> 'a * (t * 'b)

val canon_opt : astate -> needs_canon option -> t option

val canon_opt' : 
  astate ->
  Pulselib.PulseBasicInterface.AbstractValue.t option ->
  t option

val canon_opt_fst : astate -> (needs_canon * 'a) option -> (t * 'a) option

val canon_opt_fst4' : 
  astate ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * 'a * 'b * 'c) option ->
  (t * 'a * 'b * 'c) option

val mk_fresh : unit -> t

This is just AbstractValue.mk_fresh so technically is only guaranteed to produce a canonical representative if the value is not immediately made equal to another one... Use with caution!

val unsafe_cast : Pulselib.PulseBasicInterface.AbstractValue.t -> t

deprecated unsafe, obviously; please add a comment why you need to use this and suppress this warning locally with [@alert "-deprecated"]

Domain elements, revisited to be safe wrt value normalization

module Stack : sig ... end

module Memory : 
  PulseBaseMemory.S
    with type key := t
     and type in_map_t :=
           Pulselib.PulseBasicInterface.AbstractValue.t
           * Pulselib.PulseBasicInterface.ValueHistory.t
     and type out_of_map_t :=
           needs_canon * Pulselib.PulseBasicInterface.ValueHistory.t
     and type t = PulseBaseMemory.t
     and type Edges.t = PulseBaseMemory.Edges.t

val canon_access : astate -> PulseAccess.t -> Memory.Access.t

module Attributes : 
  PulseBaseAddressAttributes.S
    with type key := t
     and type t = PulseBaseAddressAttributes.t