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

Module Logging.MatchResultReport

type remaining_state = {

1. astate : AstateRec.t;
2. subst : Symbolic.Subst.t;
3. mp : Engine.MP.t;

}

val remaining_state_to_yojson : remaining_state -> Yojson.Safe.t

val remaining_state_of_yojson :
  Yojson.Safe.t ->
  remaining_state Ppx_deriving_yojson_runtime.error_or

type t =

1. | Success of{
   1. astate : AstateRec.t;
   2. subst : Symbolic.Subst.t;
   3. posts : (Gil_syntax.Flag.t * Gil_syntax.Asrt.t list) option;
   4. remaining_states : remaining_state list;
   }
2. | Failure of{
   1. cur_step : Engine.MP.step option;
   2. subst : Symbolic.Subst.t;
   3. astate : AstateRec.t;
   4. errors : err_t list;
   }

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or