package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.Constant_prop

val e2bool : Expr.pexpr -> bool Utils0.exec
val ssem_sop1 : Expr.sop1 -> Expr.pexpr -> Expr.pexpr
val ssem_sop2 : Expr.sop2 -> Expr.pexpr -> Expr.pexpr -> Expr.pexpr
val snot : Expr.pexpr -> Expr.pexpr
val sneg_int : Expr.pexpr -> Expr.pexpr
val s_op1 : Expr.sop1 -> Expr.pexpr -> Expr.pexpr
val sadd_int : Expr.pexpr -> Expr.pexpr -> Expr.pexpr
val ssub_int : Expr.pexpr -> Expr.pexpr -> Expr.pexpr
val smul_int : Expr.pexpr -> Expr.pexpr -> Expr.pexpr
val is_cmp_const : Expr.cmp_kind -> Expr.pexpr -> BinNums.coq_Z option
val app_sopn : Type.stype list -> 'a1 Utils0.exec Sem_type.sem_prod -> Expr.pexpr list -> 'a1 Utils0.exec
type const_v =
  1. | Cbool of bool
  2. | Cint of BinNums.coq_Z
  3. | Cword of Wsize.wsize * Ssralg.GRing.ComRing.sort
val const_v_beq : const_v -> const_v -> bool
val const_v_eq_axiom : const_v Eqtype.eq_axiom
val coq_HB_unnamed_factory_1 : const_v Eqtype.Coq_hasDecEq.axioms_
val constant_prop_const_v__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val const : const_v -> Expr.pexpr
type globals = (Var0.Var.var -> Global.glob_value option) option
val empty_cpm : const_v Var0.Mvar.t
val wsize_of_stype : Type.stype -> Wsize.wsize
val const_prop : 'a1 Sopn.asmOp -> (const_v Var0.Mvar.t -> 'a1 Expr.instr -> const_v Var0.Mvar.t * 'a1 Expr.instr list) -> const_v Var0.Mvar.t -> 'a1 Expr.instr list -> const_v Var0.Mvar.t * 'a1 Expr.instr list
val is_update_imm : 'a1 Sopn.asmOp -> Expr.lval list -> 'a1 Sopn.sopn -> Expr.pexpr list -> ((Expr.lval * bool) * Expr.pexpr) option