gillian » Gillian » Debugger » Utils » Match_map

Module Utils.Match_map

type kind = Engine.Matcher.match_kind

Describes why this matching is happening

val kind_to_yojson : kind -> Yojson.Safe.t

val kind_of_yojson : Yojson.Safe.t -> kind Ppx_deriving_yojson_runtime.error_or

type match_result =

1. | Success
2. | Failure

val match_result_to_yojson : match_result -> Yojson.Safe.t

val match_result_of_yojson :
  Yojson.Safe.t ->
  match_result Ppx_deriving_yojson_runtime.error_or

val pp_match_result :
  Ppx_deriving_runtime.Format.formatter ->
  match_result ->
  Ppx_deriving_runtime.unit

val show_match_result : match_result -> Ppx_deriving_runtime.string

type substitution = {

1. assert_id : Logging.Report_id.t;
2. subst : string * string;

}

A substitution, and the ID of the assertion where it was learned

val substitution_to_yojson : substitution -> Yojson.Safe.t

val substitution_of_yojson :
  Yojson.Safe.t ->
  substitution Ppx_deriving_yojson_runtime.error_or

type matching = {

1. id : Logging.Report_id.t;
2. kind : Engine.Matcher.match_kind;
3. result : match_result;

}

Data about a matching

val matching_to_yojson : matching -> Yojson.Safe.t

val matching_of_yojson :
  Yojson.Safe.t ->
  matching Ppx_deriving_yojson_runtime.error_or

type assertion_data = {

1. id : Logging.Report_id.t;
   (*

   The report ID of the assertion in the log database

   *)
2. fold : matching option;
   (*

   The ID of the fold matching and its result, if this assertion requires a fold

   *)
3. assertion : string;
   (*

   The string representation of this assertion

   *)
4. substitutions : substitution list;
   (*

   A list of the substitutions learned from this assertion specifically

   *)

}

Represents one step of a matching

val assertion_data_to_yojson : assertion_data -> Yojson.Safe.t

val assertion_data_of_yojson :
  Yojson.Safe.t ->
  assertion_data Ppx_deriving_yojson_runtime.error_or

type next = Logging.Report_id.t list

val next_to_yojson : next -> Yojson.Safe.t

val next_of_yojson : Yojson.Safe.t -> next Ppx_deriving_yojson_runtime.error_or

type step =

1. | Assertion of assertion_data
2. | RecoveryTactic of Engine.Matcher.recovery_tactic

val step_to_yojson : step -> Yojson.Safe.t

val step_of_yojson : Yojson.Safe.t -> step Ppx_deriving_yojson_runtime.error_or

type node = step * bool option * next

val node_to_yojson : node -> Yojson.Safe.t

val node_of_yojson : Yojson.Safe.t -> node Ppx_deriving_yojson_runtime.error_or

type t = {

1. kind : kind;
2. roots : Logging.Report_id.t list;
3. nodes : (Logging.Report_id.t, node) Utils.Prelude.Hashtbl.t;
4. result : match_result;

}

val to_yojson : t -> Yojson.Safe.t

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

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

module type Build = Match_map.Build

Build.f: Given the ID of a matching, build the representative matching map

module Make_builder (Verification : Engine.Verifier.S) : sig ... end