Asrt (soteria-c.Soteria_c_lib.Summary.Logic.Asrt)

module type Base = Soteria.Sym_states.Base.M(Csymex.CSYMEX).S

type !'a atom =

| Spatial of 'a
| Pure of Csymex.CSYMEX.Value.Expr.t

val pp_atom : 
  (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  'a atom ->
  Ppx_deriving_runtime.unit

val show_atom : 
  (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) ->
  'a atom ->
  Ppx_deriving_runtime.string

type !'a t = 'a atom list

val pp : 
  (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  'a t ->
  Ppx_deriving_runtime.unit

val show : 
  (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) ->
  'a t ->
  Ppx_deriving_runtime.string

val make : 
  spatial:'a list ->
  pure:Csymex.CSYMEX.Value.Expr.t list ->
  'a atom list

module Execute (B : Base) : sig ... end