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