module Cint:sig
..end
Integer Arithmetic Model
val of_real : Wp.Ctypes.c_int -> Wp.Lang.F.unop
val convert : Wp.Ctypes.c_int -> Wp.Lang.F.unop
Independent from model
val to_integer : Wp.Lang.F.unop
val of_integer : Wp.Ctypes.c_int -> Wp.Lang.F.unop
val to_cint : Wp.Lang.lfun -> Wp.Ctypes.c_int
Raises Not_found
if not.
val is_cint : Wp.Lang.lfun -> Wp.Ctypes.c_int
Raises Not_found
if not.
type
model =
| |
Natural |
| |
Machine |
val configure : model -> Wp.WpContext.rollback
val current : unit -> model
val range : Wp.Ctypes.c_int -> Wp.Lang.F.term -> Wp.Lang.F.pred
Dependent on model
val downcast : Wp.Ctypes.c_int -> Wp.Lang.F.unop
Dependent on model
val iopp : Wp.Ctypes.c_int -> Wp.Lang.F.unop
val iadd : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val isub : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val imul : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val idiv : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val imod : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val bnot : Wp.Ctypes.c_int -> Wp.Lang.F.unop
val band : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val bxor : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val bor : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val blsl : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val blsr : Wp.Ctypes.c_int -> Wp.Lang.F.binop
val l_not : Wp.Lang.F.unop
val l_and : Wp.Lang.F.binop
val l_xor : Wp.Lang.F.binop
val l_or : Wp.Lang.F.binop
val l_lsl : Wp.Lang.F.binop
val l_lsr : Wp.Lang.F.binop
val f_lnot : Wp.Lang.lfun
val f_land : Wp.Lang.lfun
val f_lxor : Wp.Lang.lfun
val f_lor : Wp.Lang.lfun
val f_lsl : Wp.Lang.lfun
val f_lsr : Wp.Lang.lfun
val f_bitwised : Wp.Lang.lfun list
All except f_bit_positive
val f_bits : Wp.Lang.lfun list
All bit-test functions
val bit_test : Wp.Lang.F.term -> int -> Wp.Lang.F.term
Simplifiers
val is_cint_simplifier : Wp.Lang.simplifier
Remove the is_cint
in formulas that are
redundant with other conditions.
val mask_simplifier : Wp.Lang.simplifier
val is_positive_or_null : Wp.Lang.F.term -> bool