Module Wp.CintSource

Integer Arithmetic Model

Independent from model

Sourceval to_integer : Lang.F.unop
Sourceval of_integer : Ctypes.c_int -> Lang.F.unop
Sourceval to_cint : Lang.lfun -> Ctypes.c_int

Raises Not_found if not.

Sourceval is_cint : Lang.lfun -> Ctypes.c_int

Raises Not_found if not.

Sourcetype model =
  1. | Natural
  2. | Machine
Sourceval configure : model -> WpContext.rollback
Sourceval current : unit -> model

Dependent on model

Dependent on model

Sourceval l_not : Lang.F.unop
Sourceval l_and : Lang.F.binop
Sourceval l_xor : Lang.F.binop
Sourceval l_lsl : Lang.F.binop
Sourceval l_lsr : Lang.F.binop
Sourceval f_lnot : Lang.lfun
Sourceval f_land : Lang.lfun
Sourceval f_lxor : Lang.lfun
Sourceval f_lor : Lang.lfun
Sourceval f_lsl : Lang.lfun
Sourceval f_lsr : Lang.lfun
Sourceval f_bitwised : Lang.lfun list

All except f_bit_positive

Sourceval f_bits : Lang.lfun list

All bit-test functions

Sourceval bit_test : Lang.F.term -> int -> Lang.F.term

Matchers

Sourceval match_power2 : Lang.F.term -> Lang.F.term
Sourceval match_power2_minus1 : Lang.F.term -> Lang.F.term

Simplifiers

Sourceval is_cint_simplifier : Lang.simplifier

Remove the is_cint in formulas that are redundant with other conditions.

Sourceval mask_simplifier : Lang.simplifier
Sourceval is_positive_or_null : Lang.F.term -> bool