Frama-C API - Cint
Integer Arithmetic Model
val of_real : Ctypes.c_int -> Lang.F.unopval convert : Ctypes.c_int -> Lang.F.unopIndependent from model
val to_integer : Lang.F.unopval of_integer : Ctypes.c_int -> Lang.F.unopval to_cint : Lang.lfun -> Ctypes.c_intRaises Not_found if not.
val is_cint : Lang.lfun -> Ctypes.c_intRaises Not_found if not.
val configure : model -> WpContext.rollbackval current : unit -> modelval range : Ctypes.c_int -> Lang.F.term -> Lang.F.predDependent on model
val downcast : Ctypes.c_int -> Lang.F.unopDependent on model
val iopp : Ctypes.c_int -> Lang.F.unopval iadd : Ctypes.c_int -> Lang.F.binopval isub : Ctypes.c_int -> Lang.F.binopval imul : Ctypes.c_int -> Lang.F.binopval idiv : Ctypes.c_int -> Lang.F.binopval imod : Ctypes.c_int -> Lang.F.binopval bnot : Ctypes.c_int -> Lang.F.unopval band : Ctypes.c_int -> Lang.F.binopval bxor : Ctypes.c_int -> Lang.F.binopval bor : Ctypes.c_int -> Lang.F.binopval blsl : Ctypes.c_int -> Lang.F.binopval blsr : Ctypes.c_int -> Lang.F.binopval l_not : Lang.F.unopval l_and : Lang.F.binopval l_xor : Lang.F.binopval l_or : Lang.F.binopval l_lsl : Lang.F.binopval l_lsr : Lang.F.binopval f_lnot : Lang.lfun Lang.externval f_land : Lang.lfun Lang.externval f_lxor : Lang.lfun Lang.externval f_lor : Lang.lfun Lang.externval f_lsl : Lang.lfun Lang.externval f_lsr : Lang.lfun Lang.externval p_bit_test : Lang.lfun Lang.externval f_bitwised : Lang.lfun Lang.extern listAll bitwise operators
val is_bitwised : Lang.lfun -> boolval bitk : Lang.F.term -> Lang.F.term -> Lang.F.termval bit_test : Lang.F.term -> Lang.F.term -> Lang.F.predval bit_testk : Lang.F.term -> int -> Lang.F.predMatchers
val match_power2 : Lang.F.term -> Lang.F.termval match_power2_minus1 : Lang.F.term -> Lang.F.termSimplifiers
val is_cint_simplifier : Lang.simplifierRemove the is_cint in formulas that are redundant with other conditions.
val mask_simplifier : Lang.simplifierval is_positive_or_null : Lang.F.term -> bool