Safety_common (p.jasmin.2026.09.0.doc.jasmin.jasmin.Jasmin.Safety

type safety_cond = Expr.eassert list

val esubtype : 
  BinNums.coq_Z Type.extended_type ->
  BinNums.coq_Z Type.extended_type ->
  bool

val etrue : Expr.pexpr

val aands : Expr.eassert list -> Expr.eassert

val to_etype : 
  Wsize.signedness option ->
  Type.atype ->
  BinNums.coq_Z Type.extended_type

val sign_of_var : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.Var.var ->
  Wsize.signedness option

val etype_of_var : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Var0.Var.var ->
  BinNums.coq_Z Type.extended_type

val sign_of_gvar : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Expr.gvar ->
  Wsize.signedness option

val etype_of_gvar : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Expr.gvar ->
  BinNums.coq_Z Type.extended_type

val sign_of_etype : BinNums.coq_Z Type.extended_type -> Wsize.signedness option

val etype_of_expr : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Expr.pexpr ->
  BinNums.coq_Z Type.extended_type

val sign_of_expr : 
  (Var0.Var.var -> (Wsize.signedness * Var0.Var.var) option) ->
  Expr.pexpr ->
  Wsize.signedness option

val elei : Expr.pexpr -> Expr.pexpr -> Expr.pexpr

val eeqi : Expr.pexpr -> Expr.pexpr -> Expr.pexpr

val eneqi : Expr.pexpr -> Expr.pexpr -> Expr.pexpr

val elsli : Expr.pexpr -> Expr.pexpr -> Expr.pexpr

val ezero : Expr.pexpr

val emin_signed : Wsize.wsize -> Expr.pexpr

val emax_signed : Wsize.wsize -> Expr.pexpr

val emax_unsigned : Wsize.wsize -> Expr.pexpr

val safety_lbl : string

val safe_assert : 
  'a1 Sopn.asmOp ->
  Expr.instr_info ->
  safety_cond ->
  'a1 Expr.instr list

val sc_in_range : Expr.pexpr -> Expr.pexpr -> Expr.pexpr -> Expr.pexpr

val sc_uint_range : Wsize.wsize -> Expr.pexpr -> Expr.pexpr

val sc_sint_range : Wsize.wsize -> Expr.pexpr -> Expr.pexpr

val sc_wi_range : Wsize.signedness -> Wsize.wsize -> Expr.pexpr -> Expr.pexpr

val is_wi1 : Operators.sop1 -> (Wsize.signedness * Operators.wiop1) option

val is_wi2 : 
  Operators.sop2 ->
  ((Wsize.signedness * Wsize.wsize) * Operators.wiop2) option

val sc_wiop1 : 
  (Wsize.signedness -> Wsize.wsize -> Expr.pexpr -> Expr.pexpr) ->
  Wsize.signedness ->
  Operators.wiop1 ->
  Expr.pexpr ->
  Expr.pexpr list

val sc_wi_range_op2 : 
  Wsize.signedness ->
  Wsize.wsize ->
  Operators.sop2 ->
  Expr.pexpr ->
  Expr.pexpr ->
  Expr.pexpr

val sc_divmod : 
  Wsize.signedness ->
  Wsize.wsize ->
  Expr.pexpr ->
  Expr.pexpr ->
  Expr.pexpr list

val sc_wiop2 : 
  Wsize.signedness ->
  Wsize.wsize ->
  Operators.wiop2 ->
  Expr.pexpr ->
  Expr.pexpr ->
  Expr.pexpr list

val sc_op1 : 
  (Wsize.signedness -> Wsize.wsize -> Expr.pexpr -> Expr.pexpr) ->
  Operators.sop1 ->
  Expr.pexpr ->
  Expr.pexpr list

val check_xs : 
  bool ->
  Var0.SvExtra.Sv.t ->
  Expr.lval list ->
  Expr.pexpr list list ->
  bool