I (transformers.States.Injector.Make.I)

type t

val pre_produce : (t * Gillian.Gil_syntax.Expr.t list) injection_hook

Called with the predicate's name and ins + outs before its production into the state. Replaces ins+outs

val pre_consume : (t * Gillian.Gil_syntax.Expr.t list) injection_hook

Called with the predicate's name and ins before its consumption from the state. Replaces ins

val post_consume : (t * Gillian.Gil_syntax.Expr.t list) injection_hook

Called with the predicate's name and outs after its consumption from the state. Replaces outs

val pre_execute_action : (t * Gillian.Gil_syntax.Expr.t list) injection_hook

Called with the action's name and args before its execution. Replaces args

val post_execute_action : 
  (t * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list)
    injection_hook

Called with the action's name and returns after its execution. Replaces returns

val post_instantiate : 
  (t * Gillian.Gil_syntax.Expr.t list) ->
  t * Gillian.Gil_syntax.Expr.t list

Called after instantiation of the state