Module ASTLanguage__ALDebugger.EvaluationTracker
type eval_result
=
|
Eval_undefined
|
Eval_true
|
Eval_false
type content
=
{
ast_node : ASTLanguage.Ctl_parser_types.ast_node;
phi : ASTLanguage.CTLTypes.t;
lcxt : ASTLanguage.CLintersContext.context;
eval_result : eval_result;
witness : ASTLanguage.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 ASTLanguage.Ctl_parser_types.ast_node
|
Last_occurrence of ASTLanguage.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 : ASTLanguage.Ctl_parser_types.ast_node -> ASTLanguage.CTLTypes.t -> ASTLanguage.CLintersContext.context -> content
val eval_begin : t -> content -> t
val eval_end : t -> ASTLanguage.Ctl_parser_types.ast_node option -> t
module DottyPrinter : sig ... end