Module Ortac_qcheck_stm.IrSource

Sourcetype new_state_formulae = {
  1. model : Ident.t;
  2. description : Gospel.Tterm.term;
}
Sourcetype term = int * Gospel.Tterm.term
Sourcetype next_state = {
  1. formulae : (int * new_state_formulae) list;
  2. modifies : (Ident.t * Ppxlib.Location.t) list;
}
Sourcetype postcond = {
  1. normal : term list;
  2. exceptional : xpost list;
  3. checks : Gospel.Tterm.term list;
}
Sourcetype value = {
  1. id : Ident.t;
  2. ty : Ppxlib.core_type;
  3. inst : (string * Ppxlib.core_type) list;
  4. sut_var : Ident.t;
  5. args : (Ppxlib.core_type * Ident.t option) list;
  6. ret : Ident.t list;
  7. next_state : next_state;
  8. precond : Gospel.Tterm.term list;
  9. postcond : postcond;
}
Sourcetype init_state = {
  1. arguments : (Gospel.Tast.lb_arg * Ppxlib.expression) list;
  2. returned_sut : Ident.t;
  3. descriptions : new_state_formulae list;
}
Sourceval get_return_type : value -> Ppxlib.core_type
Sourceval value : Ident.t -> Ppxlib.core_type -> (string * Ppxlib.core_type) list -> Ident.t -> (Ppxlib.core_type * Ident.t option) list -> Ident.t list -> next_state -> Gospel.Tterm.term list -> postcond -> value
Sourcetype t = {
  1. state : (Ident.t * Ppxlib.core_type) list;
  2. init_state : init_state;
  3. ghost_functions : Gospel.Tast.function_ list;
  4. values : value list;
}
Sourceval pp_inst : Format.formatter -> (string * Astlib.Ast_414.Parsetree.core_type) list -> unit
Sourceval pp_value : Format.formatter -> value -> unit
Sourceval pp : Format.formatter -> t -> unit