Module ALDebugger.EvaluationTracker

type eval_result =
| Eval_undefined
| Eval_true
| Eval_false
type content = {
ast_node : Ctl_parser_types.ast_node;
phi : CTLTypes.t;
lcxt : CLintersContext.context;
eval_result : eval_result;
witness : Ctl_parser_types.ast_node option;
}
type eval_node = {
id : int;
content : content;
}
type tree =
| Tree of eval_node * tree list
type ast_node_to_display =
| Carry_forward of Ctl_parser_types.ast_node
| Last_occurrence of Ctl_parser_types.ast_node
type t = {
next_id : int;
eval_stack : (tree * ast_node_to_display) IStdlib.IStd.Stack.t;
forest : tree list;
breakpoint_line : int option;
debugger_active : bool;
}
val create : IBase.SourceFile.t -> t
val create_content : Ctl_parser_types.ast_node -> CTLTypes.t -> CLintersContext.context -> content
val eval_begin : t -> content -> t
val eval_end : t -> Ctl_parser_types.ast_node option -> t
module DottyPrinter : sig ... end