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

Parameters

module B : Base

val produce_atom : 
  B.syn atom ->
  B.t option ->
  B.t option Csymex.CSYMEX.Producer.t

val produce : B.syn t -> B.t option -> B.t option Csymex.CSYMEX.Producer.t

val subst_covers : 
  Csymex.CSYMEX.Value.Expr.Subst.t ->
  Csymex.CSYMEX.Value.Expr.t ->
  bool

val ins_outs : 
  B.syn atom ->
  Csymex.CSYMEX.Value.Expr.t list * Csymex.CSYMEX.Value.Expr.t list

val is_consumable : Csymex.CSYMEX.Value.Expr.Subst.t -> B.syn atom -> bool

val consume_atom : 
  B.syn atom ->
  B.t option ->
  (B.t option, B.syn list) Csymex.CSYMEX.Consumer.t

val consume : 
  B.syn t ->
  B.t option ->
  (B.t option, B.syn list) Csymex.CSYMEX.Consumer.t