gillian » Gillian » Logging » Log_queryer

Module Logging.Log_queryer

val get_report : Logging.Report_id.t -> (string * string) option

Gets content and type (in that order) of the given ID

val get_previous_report_id : Logging.Report_id.t -> Logging.Report_id.t option

Gets the ID of the report that precedes the given ID

val get_next_reports :
  Logging.Report_id.t ->
  (Logging.Report_id.t * string * string) list

Gets the ID, content and type (in that order) of all reports that directly succeed the given ID

val get_next_report_ids : Logging.Report_id.t -> Logging.Report_id.t list

As with get_next_reports, but only gives IDs

val get_next_report_id : Logging.Report_id.t -> Logging.Report_id.t option

Gets the ID of the "first" report that succeeds the given ID

val get_previously_freed_annot : string -> string option

Gets the annotation corresponding to the previous set-freed action for a given location in the current phase, if it exists

val get_children_of :
  ?roots_only:bool ->
  Logging.Report_id.t ->
  (Logging.Report_id.t * string * string) list

Gets the ID, type, and content (in that order) of any children of the given ID

If roots_only is true, only gets children with no previous; defaults to false

val get_cmd_results :
  Logging.Report_id.t ->
  (Logging.Report_id.t * string) list

Gets the ID and content of any children of the given ID with type "cmd_result"

val get_match_for :
  Logging.Report_id.t ->
  (Logging.Report_id.t * string) option

Gets the ID and content of a child, with type "match", of the given ID (if it exists)

val get_match_results :
  Logging.Report_id.t ->
  (Logging.Report_id.t * string) list

Returns the ID and content of all children of the given ID with type "match_result"

val resolve_command_and_matches :
  Logging.Report_id.t ->
  Logging.Report_id.t * (Logging.Report_id.t * Logging.Report_id.t) list

Given an ID for an assertion, traverses parents until a command is encountered. Returns the command ID, and a list of pairs of assertion ID and respective match ID