package jasmin

  1. Overview
  2. Docs
Compiler for High-Assurance and High-Speed Cryptography

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (17)

Authors

  1. J
    Jasmin authors and contributors

Maintainers

  1. J
    Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Sources

jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa

doc/jasmin.jasmin/Jasmin/Fexpr/index.html

Module Jasmin.Fexpr

type fexpr =
  1. | Fconst of BinNums.coq_Z
  2. | Fvar of Expr.var_i
  3. | Fapp1 of Expr.sop1 * fexpr
  4. | Fapp2 of Expr.sop2 * fexpr * fexpr
  5. | Fif of fexpr * fexpr * fexpr
val fconst : Wsize.wsize -> BinNums.coq_Z -> fexpr
val fadd : Wsize.wsize -> fexpr -> fexpr -> fexpr
val faddv : Wsize.wsize -> Expr.var_i -> fexpr -> fexpr
type rexpr =
  1. | Load of Memory_model.aligned * Wsize.wsize * fexpr
  2. | Rexpr of fexpr
type lexpr =
  1. | Store of Memory_model.aligned * Wsize.wsize * fexpr
  2. | LLvar of Expr.var_i
val fexpr_of_pexpr : Expr.pexpr -> fexpr option
val rexpr_of_pexpr : Expr.pexpr -> rexpr option
val lexpr_of_lval : Expr.lval -> lexpr option
val free_vars_rec : Var0.SvExtra.Sv.t -> fexpr -> Var0.SvExtra.Sv.t
val free_vars : fexpr -> Var0.SvExtra.Sv.t
val free_vars_r : rexpr -> Var0.SvExtra.Sv.t
val rvar : Expr.var_i -> rexpr
val rconst : Wsize.wsize -> BinNums.coq_Z -> rexpr