gillian » Gillian » Debugger » Lifter » Gil_lifter » Make » Verifier » SMatcher

Module Verifier.SMatcher

type err_t

type state_t = State.t

type t = state_t

type post_res = (Gil_syntax.Flag.t * Gil_syntax.Asrt.t list) option

type search_state = (t * Symbolic.Subst.t * Engine.MP.t) list * err_t list

module Logging : sig ... end

val produce_assertion :
  t ->
  Symbolic.Subst.t ->
  Gil_syntax.Asrt.atom ->
  (t, err_t) Engine.Res_list.t

val produce :
  t ->
  Symbolic.Subst.t ->
  Gil_syntax.Asrt.t ->
  (t, err_t) Engine.Res_list.t

val produce_posts : t -> Symbolic.Subst.t -> Gil_syntax.Asrt.t list -> t list

val try_recovering :
  t ->
  Gil_syntax.Expr.t Engine.Recovery_tactic.t ->
  (t list * Engine.Matcher.recovery_tactic, string) Stdlib.result

Tries recovering from an error using the provided recovery tactic, by delegating to the predicate-carrying memory (through the reserved recover action) and simplifying the recovered states.

val match_assertion :
  ?no_auto_fold:bool ->
  t ->
  Symbolic.Subst.t ->
  Engine.MP.step ->
  (t, err_t) Engine.Res_list.t

val match_ :
  ?in_matching:bool ->
  t ->
  Symbolic.Subst.t ->
  Engine.MP.t ->
  Engine.Matcher.match_kind ->
  (t * Symbolic.Subst.t * post_res, err_t) Engine.Res_list.t