Module SAInterpreter.CConf

Type of configurations: state, call stack, previous index, previous loop ids, current index, branching

type err = {
  1. callstack : Call_stack.t;
  2. proc_idx : int;
  3. error_state : state_t;
  4. errors : err_t list;
  5. branch_path : Gillian.Gil_syntax.Branch_case.path;
  6. prev_cmd_report_id : Gillian.Logging.Report_id.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 : Gillian.Logging.Report_id.t option;
  9. branch_case : Gillian.Gil_syntax.Branch_case.t option;
  10. branch_path : Gillian.Gil_syntax.Branch_case.path;
}
type finish = {
  1. flag : Gillian.Gil_syntax.Flag.t;
  2. ret_val : state_vt;
  3. final_state : state_t;
  4. branch_path : Gillian.Gil_syntax.Branch_case.path;
  5. prev_cmd_report_id : Gillian.Logging.Report_id.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 : Gillian.Gil_syntax.Branch_case.path;
  10. prev_cmd_report_id : Gillian.Logging.Report_id.t option;
}
type t =
  1. | ConfErr of err
  2. | ConfCont of cont
  3. | ConfFinish of finish
  4. | ConfSusp of susp