sig
  type exec_mode = Exec_giant_steps | Exec_normal
  val pp_mode : Stdlib.Format.formatter -> Pinterp_core.Log.exec_mode -> unit
  type value_or_invalid = Value of Pinterp_core.Value.value | Invalid
  type log_entry_desc = private
      Val_assumed of (Why3.Ident.ident * Pinterp_core.Value.value)
    | Res_assumed of (Why3.Expr.rsymbol option * Pinterp_core.Value.value)
    | Const_init of Why3.Ident.ident
    | Exec_call of
        (Why3.Expr.rsymbol option *
         Pinterp_core.Value.value Why3.Term.Mvs.t *
         Pinterp_core.Log.exec_mode)
    | Exec_pure of (Why3.Term.lsymbol * Pinterp_core.Log.exec_mode)
    | Exec_any of
        (Why3.Expr.rsymbol option * Pinterp_core.Value.value Why3.Term.Mvs.t)
    | Iter_loop of Pinterp_core.Log.exec_mode
    | Exec_main of
        (Why3.Expr.rsymbol *
         Pinterp_core.Log.value_or_invalid Why3.Term.Mls.t *
         Pinterp_core.Value.value Why3.Term.Mvs.t *
         Pinterp_core.Log.value_or_invalid Why3.Expr.Mrs.t)
    | Exec_stucked of (string * Pinterp_core.Value.value Why3.Ident.Mid.t)
    | Exec_failed of
        (string * Pinterp_core.Log.value_or_invalid Why3.Expr.Mrs.t *
         Pinterp_core.Log.value_or_invalid Why3.Term.Mls.t *
         Pinterp_core.Value.value Why3.Term.Mvs.t *
         Pinterp_core.Value.value Why3.Ident.Mid.t)
    | Exec_ended
  type log_entry = private {
    log_desc : Pinterp_core.Log.log_entry_desc;
    log_loc : Why3.Loc.position option;
  }
  type exec_log = Pinterp_core.Log.log_entry list
  type log_uc
  val log_val :
    Pinterp_core.Log.log_uc ->
    Why3.Ident.ident ->
    Pinterp_core.Value.value -> Why3.Loc.position option -> unit
  val log_const :
    Pinterp_core.Log.log_uc ->
    Why3.Ident.ident -> Why3.Loc.position option -> unit
  val log_call :
    Pinterp_core.Log.log_uc ->
    Why3.Expr.rsymbol option ->
    Pinterp_core.Value.value Why3.Term.Mvs.t ->
    Pinterp_core.Log.exec_mode -> Why3.Loc.position option -> unit
  val log_pure_call :
    Pinterp_core.Log.log_uc ->
    Why3.Term.lsymbol ->
    Pinterp_core.Log.exec_mode -> Why3.Loc.position option -> unit
  val log_any_call :
    Pinterp_core.Log.log_uc ->
    Why3.Expr.rsymbol option ->
    Pinterp_core.Value.value Why3.Term.Mvs.t ->
    Why3.Loc.position option -> unit
  val log_iter_loop :
    Pinterp_core.Log.log_uc ->
    Pinterp_core.Log.exec_mode -> Why3.Loc.position option -> unit
  val log_exec_main :
    Pinterp_core.Log.log_uc ->
    Why3.Expr.rsymbol ->
    Pinterp_core.Value.value Stdlib.Lazy.t Why3.Term.Mls.t ->
    Pinterp_core.Value.value Why3.Term.Mvs.t ->
    Pinterp_core.Value.value Stdlib.Lazy.t Why3.Expr.Mrs.t ->
    Why3.Loc.position option -> unit
  val log_failed :
    Pinterp_core.Log.log_uc ->
    string ->
    Pinterp_core.Value.value Stdlib.Lazy.t Why3.Expr.Mrs.t ->
    Pinterp_core.Value.value Stdlib.Lazy.t Why3.Term.Mls.t ->
    Pinterp_core.Value.value Why3.Term.Mvs.t ->
    Pinterp_core.Value.value Why3.Ident.Mid.t ->
    Why3.Loc.position option -> unit
  val log_stucked :
    Pinterp_core.Log.log_uc ->
    string ->
    Pinterp_core.Value.value Why3.Ident.Mid.t ->
    Why3.Loc.position option -> unit
  val log_exec_ended :
    Pinterp_core.Log.log_uc -> Why3.Loc.position option -> unit
  val empty_log_uc : unit -> Pinterp_core.Log.log_uc
  val empty_log : Pinterp_core.Log.exec_log
  val get_log : Pinterp_core.Log.log_uc -> Pinterp_core.Log.exec_log
  val flush_log : Pinterp_core.Log.log_uc -> Pinterp_core.Log.exec_log
  val sort_log_by_loc :
    Pinterp_core.Log.exec_log ->
    Pinterp_core.Log.log_entry list Why3.Wstdlib.Mint.t Why3.Wstdlib.Mstr.t
  val json_log : Pinterp_core.Log.exec_log -> Why3.Json_base.json
  val print_log : ?verb_lvl:int -> Pinterp_core.Log.exec_log Why3.Pp.pp
  val get_exec_calls_and_loops :
    Why3.Env.env ->
    Pinterp_core.Log.exec_log -> Pinterp_core.Log.log_entry list
end