package jasmin

You can search for identifiers within the package.

in-package search v0.2.0

jasmin
- README
- Library jasmin.jasmin
  - Jasmin
    
    Alias
    
    Allocation
    
    E
    
    M
    
    Mv
    
    Annot
    
    Annotations
    
    Arch_decl
    
    Arch_extra
    
    MkToIdent_T
    
    MkToIdent
    
    AToIdent_T
    
    MkAToIdent
    
    Arch_full
    
    Core_arch
    
    Arch
    
    Arch_from_Core_arch
    
    Arch_params
    
    Arch_utils
    
    Arm
    
    Arm_arch_full
    
    Arm_input
    
    Arm_core
    
    Arm
    
    Arm_decl
    
    Arm_expand_imm
    
    Arm_extra
    
    E
    
    Arm_instr_decl
    
    E
    
    Arm_lowering
    
    Arm_params
    
    Arm_params_common
    
    ARMFopn
    
    Arm_params_core
    
    ARMFopn_core
    
    Arm_stack_zeroization
    
    Array_copy
    
    E
    
    Array_expand
    
    Array_expansion
    
    E
    
    Array_init
    
    Ascii
    
    AsmTargetBuilder
    
    AsmTarget
    
    S
    
    Make
    
    Asm_gen
    
    E
    
    Asm_utils
    
    Bigop
    
    Coq_bigop_Locked
    
    Coq_bigop
    
    BinInt
    
    Z
    
    BinNat
    
    N
    
    BinNums
    
    BinPos
    
    Pos
    
    BinPosDef
    
    Pos
    
    Bool
    
    CLI_errors
    
    CMorphisms
    
    CRelationClasses
    
    CheckAnnot
    
    Choice
    
    CodeSeq
    
    Coq_hasChoice
    
    Choice
    
    Exports
    
    Choice_isCountable
    
    Countable
    
    Exports
    
    Coq_isCountable
    
    Builders_77
    
    Compile
    
    Compiler
    
    Compiler_util
    
    LoopCounter
    
    Loop
    
    Constant_prop
    
    Constraints
    
    Vl
    
    Svl
    
    Mvl
    
    Hvl
    
    Lvl
    
    C
    
    VlPairs
    
    Conv
    
    CoreArchFactory
    
    Core_arch_ARM
    
    Core_arch_RISCV
    
    CoreConv
    
    CoreIdent
    
    L
    
    Name
    
    GV
    
    V
    
    Cident
    
    F
    
    Sf
    
    Exceptionless
    
    Labels
    
    Mf
    
    Exceptionless
    
    Infix
    
    Labels
    
    Hf
    
    Exceptionless
    
    Infix
    
    Labels
    
    Ct_checker_forward
    
    Datatypes
    
    Dead_calls
    
    E
    
    Dead_code
    
    E
    
    DebugInfo
    
    DecidableType
    
    DecidableType
    
    Div
    
    EqbOK
    
    Eqb_core_defs
    
    EqdepFacts
    
    Eqtype
    
    Coq_hasDecEq
    
    Equality
    
    Coq_isSub
    
    SubType
    
    Equalities
    
    DecidableType
    
    DecidableTypeOrig
    
    Evaluator
    
    Expr
    
    TAG
    
    VarInfo
    
    InstrInfoT
    
    InstrInfo
    
    FunInfoT
    
    FunInfo
    
    FInfo
    
    FMapAVL
    
    Raw
    
    Proofs
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    L
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    IntMake
    
    E
    
    Raw
    
    Proofs
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    L
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    Make
    
    E
    
    Raw
    
    Proofs
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    L
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    FMapFacts
    
    WFacts_fun
    
    FMapList
    
    Raw
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    Fexpr
    
    Finfun
    
    Coq_finfun_Locked
    
    Coq_finfun
    
    Fintype
    
    Coq_isFinite
    
    Finite
    
    Exports
    
    FiniteNES
    
    Finite
    
    Coq_enum_Locked
    
    Coq_enum
    
    Flag_combination
    
    Gen_map
    
    CmpType
    
    MkOrdT
    
    MAP
    
    K
    
    Mmake
    
    K
    
    Ordered
    
    Map
    
    E
    
    Raw
    
    Proofs
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    L
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    Facts
    
    CmpZ
    
    Mz
    
    K
    
    Ordered
    
    Map
    
    E
    
    Raw
    
    Proofs
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    L
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    Facts
    
    MkMOrdT
    
    Smake
    
    Ordered
    
    Raw
    
    MX
    
    OrderTac
    
    OTF
    
    TO
    
    L
    
    MO
    
    OrderTac
    
    OTF
    
    TO
    
    E
    
    Glob_options
    
    Global
    
    Help
    
    IInfo
    
    Ident
    
    CORE_IDENT
    
    Cident
    
    Tident
    
    CmpT
    
    Mt
    
    K
    
    St
    
    Ordered
    
    Raw
    
    MX
    
    OrderTac
    
    OTF
    
    TO
    
    L
    
    MO
    
    OrderTac
    
    OTF
    
    TO
    
    E
    
    StP
    
    MP
    
    Dec
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    FM
    
    StD
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    WrapIdent
    
    IDENT
    
    Mid
    
    K
    
    Ident
    
    Mid
    
    K
    
    Init
    
    Inline
    
    E
    
    Insert_copy_and_fix_length
    
    Int
    
    Int
    
    Z_as_Int
    
    Interval
    
    IntervalGraphColoring
    
    Label
    
    Label_check
    
    Latex_printer
    
    Lea
    
    Lexer
    
    L
    
    S
    
    Linear
    
    Linear_util
    
    Linearization
    
    E
    
    List0
    
    Liveness
    
    Load_constants_in_cond
    
    E
    
    Location
    
    Low_memory
    
    Memory
    
    Lower_spill
    
    E
    
    Lowering
    
    MSetDecide
    
    WDecideOn
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    WDecide
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    MSetEqProperties
    
    WEqPropertiesOn
    
    MP
    
    Dec
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    FM
    
    WEqProperties
    
    MP
    
    Dec
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    FM
    
    EqProperties
    
    MP
    
    Dec
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    FM
    
    MSetFacts
    
    WFactsOn
    
    MSetInterface
    
    WSets
    
    E
    
    MSetProperties
    
    WPropertiesOn
    
    Dec
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    FM
    
    MakeReferenceArguments
    
    E
    
    Memory_example
    
    MemoryI
    
    Memory_model
    
    LE
    
    CoreMem
    
    MemoryT
    
    Merge_varmaps
    
    E
    
    Nat0
    
    One_varmap
    
    Order
    
    Order
    
    Coq_isPOrder
    
    POrder
    
    LtLe_isPOrder
    
    Builders_6
    
    OrderedType
    
    OrderedType
    
    OrderedTypeFacts
    
    TO
    
    IsTO
    
    OrderTac
    
    KeyOrderedType
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    Orders
    
    EqLtLe
    
    OrdersTac
    
    MakeOrderTac
    
    Oseq
    
    Param1
    
    Coq_exports
    
    Param1_trivial
    
    Coq_exports
    
    Parseio
    
    Parser
    
    MenhirInterpreter
    
    Incremental
    
    PeanoNat
    
    Nat
    
    Post_unrolling_check
    
    E
    
    Pp_arm_m4
    
    Pp_riscv
    
    Pp_stack_alloc
    
    Pp_x86
    
    Prelude
    
    Pretyping
    
    Env
    
    Funs
    
    Exec
    
    PrimInt63
    
    PrintASM
    
    PrintCommon
    
    PrintFexpr
    
    PrintLinear
    
    Printer
    
    Prog
    
    L
    
    Name
    
    GV
    
    Cident
    
    F
    
    Sf
    
    Mf
    
    Hf
    
    E
    
    PV
    
    Mpv
    
    Exceptionless
    
    Infix
    
    Labels
    
    Spv
    
    Exceptionless
    
    Labels
    
    V
    
    Sv
    
    Exceptionless
    
    Labels
    
    Mv
    
    Exceptionless
    
    Infix
    
    Labels
    
    Hv
    
    Exceptionless
    
    Infix
    
    Labels
    
    Propagate_inline
    
    E
    
    Psem_defs
    
    Pseudo_operator
    
    Puf
    
    Regalloc
    
    Regalloc
    
    Regalloc
    
    RemoveUnusedResults
    
    Remove_globals
    
    E
    
    Riscv
    
    Riscv_arch_full
    
    Riscv_input
    
    Riscv_core
    
    Riscv
    
    Riscv_decl
    
    Riscv_extra
    
    E
    
    Riscv_instr_decl
    
    E
    
    Riscv_lower_addressing
    
    E
    
    Riscv_lowering
    
    Riscv_params
    
    Riscv_params_common
    
    RISCVFopn
    
    Riscv_params_core
    
    RISCVFopn_core
    
    Riscv_stack_zeroization
    
    Sct_checker_forward
    
    SecurityAnnotations
    
    PP
    
    Parse
    
    Sem_op_typed
    
    Sem_params
    
    Sem_params_of_arch_extra
    
    Sem_type
    
    Seq
    
    Seq_extra
    
    Sha256
    
    Shift_kind
    
    Slh_lowering
    
    E
    
    Env
    
    Slh_ops
    
    Slicing
    
    Sopn
    
    Specif
    
    Ssa
    
    Ssralg
    
    GRing
    
    Coq_isNmodule
    
    Nmodule
    
    Nmodule_isZmodule
    
    Zmodule
    
    Exports
    
    Coq_isZmodule
    
    Builders_8
    
    Nmodule_isSemiRing
    
    SemiRing
    
    Exports
    
    Ring
    
    Exports
    
    Zmodule_isRing
    
    Builders_31
    
    SemiRing_hasCommutativeMul
    
    ComRing
    
    Exports
    
    Ring_hasCommutativeMul
    
    Builders_206
    
    Zmodule_isComRing
    
    Builders_211
    
    Ring_hasMulInverse
    
    ComRing_hasMulInverse
    
    Builders_256
    
    ComUnitRing_isIntegral
    
    IntegralDomain
    
    Ssrbool
    
    PredOfSimpl
    
    Ssreflect
    
    Ssrfun
    
    Option
    
    Ssrint
    
    Coq_intZmod
    
    Ssrnat
    
    Ssrnum
    
    Num
    
    POrderedZmodule
    
    Exports
    
    IntegralDomain_isNumRing
    
    Builders_57
    
    IntegralDomain_isLeReal
    
    Builders_73
    
    StackAlloc
    
    StackAlloc
    
    Stack_alloc
    
    E
    
    CmpR
    
    Mr
    
    K
    
    Ordered
    
    Map
    
    E
    
    Raw
    
    Proofs
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    L
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    Facts
    
    Stack_alloc_params
    
    Stack_zero_strategy
    
    Stack_zeroization
    
    E
    
    Std
    
    Prelude
    
    String0
    
    Subst
    
    Sumbool
    
    Syntax
    
    L
    
    W
    
    Syscall
    
    Syscall_ocaml
    
    Syscall_sem
    
    Syscall_t
    
    Tagged
    
    TaggedCore
    
    Tagged
    
    CmpT
    
    Mt
    
    K
    
    St
    
    Ordered
    
    Raw
    
    MX
    
    OrderTac
    
    OTF
    
    TO
    
    L
    
    MO
    
    OrderTac
    
    OTF
    
    TO
    
    E
    
    StP
    
    MP
    
    Dec
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    FM
    
    StD
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    ToEC
    
    Tt_arm_m4
    
    Tunneling
    
    E
    
    Tuple
    
    Type
    
    OtherDefs
    
    Typing
    
    Uint0
    
    UnionFindBasic
    
    Unionfind
    
    EqType
    
    NaiveUnionFind
    
    LblEqType
    
    LUF
    
    Unrolling
    
    Utils
    
    Set
    
    OrderedType
    
    S
    
    Exceptionless
    
    Labels
    
    Make
    
    Exceptionless
    
    Labels
    
    Make2
    
    Product
    
    Exceptionless
    
    Labels
    
    Int
    
    Exceptionless
    
    Labels
    
    Int32
    
    Exceptionless
    
    Labels
    
    Int64
    
    Exceptionless
    
    Labels
    
    Nativeint
    
    Exceptionless
    
    Labels
    
    Float
    
    Exceptionless
    
    Labels
    
    Char
    
    Exceptionless
    
    Labels
    
    String
    
    Exceptionless
    
    Labels
    
    Incubator
    
    PSet
    
    Map
    
    S
    
    Exceptionless
    
    Infix
    
    Labels
    
    Make
    
    Exceptionless
    
    Infix
    
    Labels
    
    Int
    
    Exceptionless
    
    Infix
    
    Labels
    
    Int32
    
    Exceptionless
    
    Infix
    
    Labels
    
    Int64
    
    Exceptionless
    
    Infix
    
    Labels
    
    Nativeint
    
    Exceptionless
    
    Infix
    
    Labels
    
    Float
    
    Exceptionless
    
    Infix
    
    Labels
    
    Char
    
    Exceptionless
    
    Infix
    
    Labels
    
    String
    
    Exceptionless
    
    Infix
    
    Labels
    
    Exceptionless
    
    Infix
    
    PMap
    
    Exceptionless
    
    Infix
    
    Hash
    
    Exceptionless
    
    Infix
    
    Labels
    
    HashedType
    
    S
    
    Exceptionless
    
    Infix
    
    Labels
    
    Make
    
    Exceptionless
    
    Infix
    
    Labels
    
    Cap
    
    Exceptionless
    
    Labels
    
    Sint
    
    Exceptionless
    
    Labels
    
    Mint
    
    Exceptionless
    
    Infix
    
    Labels
    
    Ss
    
    Exceptionless
    
    Labels
    
    Ms
    
    Exceptionless
    
    Infix
    
    Labels
    
    Hiloc
    
    Exceptionless
    
    Infix
    
    Labels
    
    Miloc
    
    Exceptionless
    
    Infix
    
    Labels
    
    Siloc
    
    Exceptionless
    
    Labels
    
    Option
    
    Monad
    
    Labels
    
    Infix
    
    Uniq
    
    ISet
    
    String
    
    IString
    
    NumString
    
    Exceptionless
    
    Cap
    
    Exceptionless
    
    IO
    
    BigEndian
    
    in_channel
    
    out_channel
    
    in_chars
    
    out_chars
    
    Buffer
    
    List
    
    Eq
    
    Ord
    
    Comp
    
    Exceptionless
    
    Infix
    
    Labels
    
    LExceptionless
    
    Parallel
    
    Utils0
    
    FinIsCount
    
    EqType
    
    FinType
    
    FinMap
    
    Result
    
    Option
    
    Values
    
    Var0
    
    FunName
    
    TFunName
    
    CmpT
    
    Mt
    
    K
    
    St
    
    Ordered
    
    Raw
    
    MX
    
    OrderTac
    
    OTF
    
    TO
    
    L
    
    MO
    
    OrderTac
    
    OTF
    
    TO
    
    E
    
    StP
    
    MP
    
    Dec
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    FM
    
    StD
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    Mf
    
    K
    
    Sf
    
    Ordered
    
    Raw
    
    MX
    
    OrderTac
    
    OTF
    
    TO
    
    L
    
    MO
    
    OrderTac
    
    OTF
    
    TO
    
    E
    
    MvMake
    
    Var
    
    CmpVar
    
    SExtra
    
    Sv
    
    Ordered
    
    Raw
    
    MX
    
    OrderTac
    
    OTF
    
    TO
    
    L
    
    MO
    
    OrderTac
    
    OTF
    
    TO
    
    E
    
    SvP
    
    MP
    
    Dec
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    FM
    
    SvD
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    SvExtra
    
    Sv
    
    Ordered
    
    Raw
    
    MX
    
    OrderTac
    
    OTF
    
    TO
    
    L
    
    MO
    
    OrderTac
    
    OTF
    
    TO
    
    E
    
    SvP
    
    MP
    
    Dec
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    FM
    
    SvD
    
    F
    
    MSetLogicalFacts
    
    MSetDecideAuxiliary
    
    MSetDecideTestCases
    
    Mvar
    
    K
    
    Ordered
    
    Map
    
    E
    
    Raw
    
    Proofs
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    L
    
    MX
    
    TO
    
    IsTO
    
    OrderTac
    
    PX
    
    MO
    
    TO
    
    IsTO
    
    OrderTac
    
    Facts
    
    Varalloc
    
    Varmap
    
    VM
    
    Vm
    
    Waes
    
    Warray_
    
    WArray
    
    Wint_int
    
    E
    
    Wint_word
    
    Word
    
    Word0
    
    Word_ssrZ
    
    ZUnitRing
    
    ZNumDomain
    
    Wsize
    
    X86
    
    X86_arch_full
    
    X86_input
    
    X86_core
    
    X86
    
    X86_decl
    
    X86_extra
    
    E
    
    X86_instr_decl
    
    X86_lowering
    
    X86_params
    
    X86_stack_zeroization
    
    Xseq
    
    Zpower
- Library jasmin.uint63
  - Uint63
- Library jasmin.uint63-js
  - Uint63
- Library jasmin.uint63-native
  - Uint63
- Sources
  - jasmin.jasmin
    
    AsmTargetBuilder.ml
    
    CLI_errors.ml
    
    UnionFindBasic.ml
    
    alias.ml
    
    annot.ml
    
    annotations.ml
    
    arch_full.ml
    
    arm_arch_full.ml
    
    array_expand.ml
    
    asm_utils.ml
    
    checkAnnot.ml
    
    compile.ml
    
    constraints.ml
    
    conv.ml
    
    coreArchFactory.ml
    
    coreConv.ml
    
    coreIdent.ml
    
    ct_checker_forward.ml
    
    debugInfo.ml
    
    evaluator.ml
    
    fInfo.ml
    
    glob_options.ml
    
    help.ml
    
    iInfo.ml
    
    insert_copy_and_fix_length.ml
    
    interval.ml
    
    intervalGraphColoring.ml
    
    jasmin.ml
    
    label_check.ml
    
    latex_printer.ml
    
    lexer.ml
    
    liveness.ml
    
    location.ml
    
    parseio.ml
    
    parser.ml
    
    pp_arm_m4.ml
    
    pp_riscv.ml
    
    pp_stack_alloc.ml
    
    pp_x86.ml
    
    pretyping.ml
    
    printASM.ml
    
    printCommon.ml
    
    printFexpr.ml
    
    printLinear.ml
    
    printer.ml
    
    prog.ml
    
    puf.ml
    
    regalloc.ml
    
    removeUnusedResults.ml
    
    riscv_arch_full.ml
    
    sct_checker_forward.ml
    
    securityAnnotations.ml
    
    slicing.ml
    
    ssa.ml
    
    stackAlloc.ml
    
    subst.ml
    
    syntax.ml
    
    syscall_ocaml.ml
    
    syscall_t.ml
    
    toEC.ml
    
    tt_arm_m4.ml
    
    typing.ml
    
    utils.ml
    
    varalloc.ml
    
    x86_arch_full.ml
  - jasmin.uint63-js
    
    uint63.ml
    
    uint63__uint63_js__.ml
  - jasmin.uint63-native
    
    uint63.ml
    
    uint63__uint63_native__.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Jasmin.Riscv_params`

val riscv_immediate : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Riscv_extra.riscv_extended_op Expr.instr_r

val riscv_saparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Stack_alloc_params.stack_alloc_params

val riscv_allocate_stack_frame : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list
    * (Riscv_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arch_utils.empty,
        Riscv_decl.condt,
        Riscv_instr_decl.riscv_op,
        Riscv_extra.riscv_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Fexpr.rexpr list)
    list

val riscv_free_stack_frame : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list
    * (Riscv_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arch_utils.empty,
        Riscv_decl.condt,
        Riscv_instr_decl.riscv_op,
        Riscv_extra.riscv_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Fexpr.rexpr list)
    list

val riscv_set_up_sp_register : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Wsize.wsize ->
  Expr.var_i ->
  Expr.var_i ->
  ((Fexpr.lexpr list
    * (Riscv_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arch_utils.empty,
        Riscv_decl.condt,
        Riscv_instr_decl.riscv_op,
        Riscv_extra.riscv_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Fexpr.rexpr list)
    list

val riscv_tmp : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Ident.Ident.ident

val riscv_tmp2 : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Ident.Ident.ident

val riscv_lmove : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  (Fexpr.lexpr list * Riscv_extra.riscv_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val riscv_check_ws : Eqtype.Equality.sort -> bool

val riscv_lstore : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Expr.var_i ->
  (Fexpr.lexpr list * Riscv_extra.riscv_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val riscv_lload : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  (Fexpr.lexpr list * Riscv_extra.riscv_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val riscv_liparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Linearization.linearization_params

val riscv_loparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  ((Riscv_decl.register,
     Arch_utils.empty,
     Arch_utils.empty,
     Arch_utils.empty,
     Riscv_decl.condt,
     Riscv_instr_decl.riscv_op,
     Riscv_extra.riscv_extra_op)
     Arch_extra.extended_op,
    Riscv_lowering.lowering_options)
    Arch_params.lowering_params

val riscv_shparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Slh_lowering.sh_params

val condt_not : Riscv_decl.condt -> Riscv_decl.condt

val assemble_cond_arg : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.instr_info ->
  Fexpr.fexpr ->
  Riscv_decl.register option Compiler_util.cexec

val assemble_cond_app2 : Expr.sop2 -> (Riscv_decl.condition_kind * bool) option

val assemble_cond : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.instr_info ->
  Fexpr.fexpr ->
  Riscv_decl.condt Compiler_util.cexec

val is_valid_address : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_decl.reg_address ->
  bool

val riscv_agparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Asm_gen.asm_gen_params

val riscv_szparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Stack_zeroization.stack_zeroization_params

val riscv_laparams : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_params.lower_addressing_params

val riscv_is_move_op : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Sopn.asm_op_t ->
  bool

val riscv_params : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op,
    Riscv_lowering.lowering_options)
    Arch_params.architecture_params

package jasmin

Module Jasmin.Riscv_params

Module `Jasmin.Riscv_params`