Evaluator (p.jasmin.2026.09.0.doc.jasmin.jasmin.Jasmin.Evaluator)

Sourceexception Eval_error of Expr.instr_info * Utils0.error

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.values

Source

val initial_memory : 
  Wsize.wsize ->
  Z.t ->
  (Z.t * Z.t) list ->
  Low_memory.Memory.mem Utils0.exec

Source

val run : 
  (module Arch_full.Arch
    with type asm_op = 'asm_op
     and type extra_op = 'extra_op) ->
  ('asm_op, 'extra_op) Arch_extra.extended_op_gen Expr.uprog ->
  Expr.instr_info ->
  CoreIdent.funname ->
  Values.value list ->
  Low_memory.Memory.mem ->
  Low_memory.Memory.mem * Values.values

Sourceval pp_val : Format.formatter -> Values.value -> unit

Sourceval pp_error : Format.formatter -> Utils0.error -> unit