package jasmin

  1. Overview
  2. Docs

Module Jasmin.Sem_params

type 'syscall_state coq_EstateParams = {
  1. _pd : Wsize.coq_PointerData;
  2. _msf_size : Wsize.coq_MSFsize;
}
val _pd : 'a1 coq_EstateParams -> Wsize.coq_PointerData
val _msf_size : 'a1 coq_EstateParams -> Wsize.coq_MSFsize
val _fcp : coq_SemPexprParams -> Flag_combination.coq_FlagCombinationParams
type ('asm_op, 'syscall_state) coq_SemInstrParams = {
  1. _asmop : 'asm_op Sopn.asmOp;
  2. _sc_sem : 'syscall_state Syscall.syscall_sem;
}
val _asmop : ('a1, 'a2) coq_SemInstrParams -> 'a1 Sopn.asmOp
val _sc_sem : ('a1, 'a2) coq_SemInstrParams -> 'a2 Syscall.syscall_sem
type coq_WithAssert = bool
val assert_allowed : coq_WithAssert -> bool
val noassert : coq_WithAssert
val withassert : coq_WithAssert