package frama-c

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

Module Wp.CintSource

Integer Arithmetic Model

Independent from model

Sourceval to_integer : Lang.F.unop
Sourceval of_integer : Ctypes.c_int -> Lang.F.unop
Sourceval to_cint : Lang.lfun -> Ctypes.c_int

Raises Not_found if not.

Sourceval is_cint : Lang.lfun -> Ctypes.c_int

Raises Not_found if not.

Sourcetype model =
  1. | Natural
  2. | Machine
Sourceval configure : model -> WpContext.rollback
Sourceval current : unit -> model

Dependent on model

Dependent on model

Sourceval l_not : Lang.F.unop
Sourceval l_and : Lang.F.binop
Sourceval l_xor : Lang.F.binop
Sourceval l_lsl : Lang.F.binop
Sourceval l_lsr : Lang.F.binop
Sourceval f_lnot : Lang.lfun
Sourceval f_land : Lang.lfun
Sourceval f_lxor : Lang.lfun
Sourceval f_lor : Lang.lfun
Sourceval f_lsl : Lang.lfun
Sourceval f_lsr : Lang.lfun
Sourceval f_bitwised : Lang.lfun list

All except f_bit_positive

Sourceval f_bits : Lang.lfun list

All bit-test functions

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

Matchers

Sourceval match_power2 : Lang.F.term -> Lang.F.term
Sourceval match_power2_minus1 : Lang.F.term -> Lang.F.term

Simplifiers

Sourceval is_cint_simplifier : Lang.simplifier

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

Sourceval mask_simplifier : Lang.simplifier
Sourceval 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