gillian » Gillian » Debugger » Lifter » Gil_fallback_lifter » Make » V » SAInterpreter » CConf

Module SAInterpreter.CConf

type err = {

1. callstack : Call_stack.t;
2. proc_idx : int;
3. error_state : state_t;
4. errors : err_t list;
5. branch_path : Gil_syntax.Branch_case.path;
6. prev_cmd_report_id : Logging.Report_id.t option;
7. loc : Utils.Location.t option;

}

type cont = {

1. state : state_t;
2. callstack : Call_stack.t;
3. invariant_frames : invariant_frames;
4. prev_idx : int;
5. next_idx : int;
6. loop_ids : string list;
7. branch_count : int;
8. prev_cmd_report_id : Logging.Report_id.t option;
9. branch_case : Gil_syntax.Branch_case.t option;
10. branch_path : Gil_syntax.Branch_case.path;
11. laction_fuel : int;
12. loc : Utils.Location.t option;

}

type finish = {

1. flag : Gil_syntax.Flag.t;
2. ret_val : state_vt;
3. final_state : state_t;
4. branch_path : Gil_syntax.Branch_case.path;
5. prev_cmd_report_id : Logging.Report_id.t option;
6. loc : Utils.Location.t option;

}

Equal to conf_cont + the id of the required spec

type susp = {

1. spec_id : string;
2. state : state_t;
3. callstack : Call_stack.t;
4. invariant_frames : invariant_frames;
5. prev_idx : int;
6. next_idx : int;
7. loop_ids : string list;
8. branch_count : int;
9. branch_path : Gil_syntax.Branch_case.path;
10. prev_cmd_report_id : Logging.Report_id.t option;
11. loc : Utils.Location.t option;

}

type t =

1. | ConfErr of err
2. | ConfCont of cont
3. | ConfFinish of finish
4. | ConfSusp of susp