package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 =
  1. | Natural
  2. | Machine
val configure : model -> WpContext.rollback
val current : unit -> model

Dependent on model

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

Dependent on model

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct