Module Cint

module Cint: sig .. end
Integer Arithmetic Model

Integer arithmetics with no upper-bound


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

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