Module Cint

module Cint: sig .. end

Integer Arithmetic Model

val of_real : Ctypes.c_int -> Lang.F.unop

val convert : Ctypes.c_int -> Lang.F.unop

Independent from model

val to_integer : Lang.F.unop

val of_integer : Ctypes.c_int -> Lang.F.unop

val to_cint : Lang.lfun -> Ctypes.c_int

Raises Not_found if not.

val is_cint : Lang.lfun -> Ctypes.c_int

Raises Not_found if not.

type model =

`\|`	`Natural`	`(*`	Integer arithmetics with no upper-bound	`*)`
`\|`	`Machine`	`(*`	Integer/Module wrt Kernel options on RTE	`*)`

val configure : model -> WpContext.rollback

val current : unit -> model

val range : Ctypes.c_int -> Lang.F.term -> Lang.F.pred

Dependent on model

val downcast : Ctypes.c_int -> Lang.F.unop

Dependent on model

val iopp : Ctypes.c_int -> Lang.F.unop

val iadd : Ctypes.c_int -> Lang.F.binop

val isub : Ctypes.c_int -> Lang.F.binop

val imul : Ctypes.c_int -> Lang.F.binop

val idiv : Ctypes.c_int -> Lang.F.binop

val imod : Ctypes.c_int -> Lang.F.binop

val bnot : Ctypes.c_int -> Lang.F.unop

val band : Ctypes.c_int -> Lang.F.binop

val bxor : Ctypes.c_int -> Lang.F.binop

val bor : Ctypes.c_int -> Lang.F.binop

val blsl : Ctypes.c_int -> Lang.F.binop

val blsr : Ctypes.c_int -> Lang.F.binop

val l_not : Lang.F.unop

val l_and : Lang.F.binop

val l_xor : Lang.F.binop

val l_or : Lang.F.binop

val l_lsl : Lang.F.binop

val l_lsr : Lang.F.binop

val f_lnot : Lang.lfun

val f_land : Lang.lfun

val f_lxor : Lang.lfun

val f_lor : Lang.lfun

val f_lsl : Lang.lfun

val f_lsr : Lang.lfun

val f_bitwised : Lang.lfun list

All except f_bit_positive

val f_bits : Lang.lfun list

All bit-test functions

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

Matchers

val match_power2 : Lang.F.term -> Lang.F.term

val match_power2_minus1 : Lang.F.term -> Lang.F.term

Simplifiers

val is_cint_simplifier : Lang.simplifier

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

val mask_simplifier : Lang.simplifier

val is_positive_or_null : Lang.F.term -> bool