PulseModelsDSL (infer.Pulselib.PulseModelsDSL)

type 'a model_monad

type astate = Pulselib.PulseDomainInterface.AbductiveDomain.t

type aval =
  Pulselib.PulseBasicInterface.AbstractValue.t
  * Pulselib.PulseBasicInterface.ValueHistory.t

val pp_aval : 
  Stdlib.Format.formatter ->
  (Pulselib.PulseBasicInterface.AbstractValue.t * 'a) ->
  unit

module Syntax : sig ... end

val unsafe_to_astate_transformer : 
  PulseBasicInterface.unsat_info ->
  'a model_monad ->
  (Pulselib.PulseBasicInterface.CallEvent.t * PulseModelsImport.model_data) ->
  astate ->
  ('a * astate) PulseBasicInterface.sat_unsat_t

warning: the transformation will fail if the result of the computation is not a single abstract state with no error and it ignores the non-disjunctive state. You should think twice before using it...