package jasmin

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Linear

type 'asm_op linstr_r =
  1. | Lopn of Fexpr.lexpr list * 'asm_op Sopn.sopn * Fexpr.rexpr list
  2. | Lsyscall of BinNums.positive Syscall_t.syscall_t
  3. | Lcall of Expr.var_i option * Label.remote_label
  4. | Lret
  5. | Lalign
  6. | Llabel of Label.label_kind * Label.label
  7. | Lgoto of Label.remote_label
  8. | Ligoto of Fexpr.rexpr
  9. | LstoreLabel of Var0.Var.var * Label.label
  10. | Lcond of Fexpr.fexpr * Label.label
type 'asm_op linstr = {
  1. li_ii : Expr.instr_info;
  2. li_i : 'asm_op linstr_r;
}
type 'asm_op lcmd = 'asm_op linstr list
type 'asm_op lfundef = {
  1. lfd_info : Expr.fun_info;
  2. lfd_align : Wsize.wsize;
  3. lfd_tyin : Type.stype list;
  4. lfd_arg : Expr.var_i list;
  5. lfd_body : 'asm_op lcmd;
  6. lfd_tyout : Type.stype list;
  7. lfd_res : Expr.var_i list;
  8. lfd_export : bool;
  9. lfd_callee_saved : Var0.Var.var list;
  10. lfd_stk_max : BinNums.coq_Z;
  11. lfd_frame_size : BinNums.coq_Z;
  12. lfd_align_args : Wsize.wsize list;
}
val lfd_total_stack : 'a1 Sopn.asmOp -> 'a1 lfundef -> BinNums.coq_Z
type 'asm_op lprog = {
  1. lp_rip : Ident.Ident.ident;
  2. lp_rsp : Ident.Ident.ident;
  3. lp_globs : Ssralg.GRing.ComRing.sort list;
  4. lp_glob_names : ((Var0.Var.var * Wsize.wsize) * BinNums.coq_Z) list;
  5. lp_funcs : (Var0.funname * 'asm_op lfundef) list;
}
val li_of_fopn_args : 'a1 Sopn.asmOp -> Expr.instr_info -> ((Fexpr.lexpr list * 'a1 Sopn.sopn) * Fexpr.rexpr list) -> 'a1 linstr