package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa
doc/jasmin.jasmin/Jasmin/Evaluator/index.html
Module Jasmin.EvaluatorSource
Source
val exec :
'syscall_state Sem_params.coq_EstateParams ->
Sem_params.coq_SemPexprParams ->
('asm_op, 'syscall_state) Sem_params.coq_SemInstrParams ->
'syscall_state ->
'asm_op Expr.prog ->
Expr.instr_info ->
Prog.funname ->
Values.values ->
Low_memory.Memory.mem ->
Low_memory.Memory.mem * Values.valuesSource
val initial_memory :
Wsize.wsize ->
Z.t ->
(Z.t * Z.t) list ->
Low_memory.Memory.mem Utils0.execSource
val run :
(module Arch_full.Arch
with type asm_op = 'asm_op
and type cond = 'cond
and type extra_op = 'extra_op
and type reg = 'reg
and type regx = 'regx
and type rflag = 'rflag
and type xreg = 'xreg) ->
('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op)
Arch_extra.extended_op
Expr.uprog ->
Expr.instr_info ->
CoreIdent.funname ->
Values.value list ->
Low_memory.Memory.mem ->
Low_memory.Memory.mem * Values.values