package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/Nat/index.html

Module `Frama_c_kernel.Nat`

Encoding of the Peano arithmetic in OCaml type system. A value of type n nat contains n at the value and the type level, allowing to express properties on objects sizes and accesses for example. It is used by the module Linear to represent vectors and matrices dimensions.

type zero = |

type 'n succ = |

type 'n nat

type positive_or_null =

| PositiveOrNull : 'n nat -> positive_or_null

type strictly_positive =

| StrictlyPositive : 'n succ nat -> strictly_positive

val zero : zero nat

val one : zero succ nat

val succ : 'n nat -> 'n succ nat

val prev : 'n succ nat -> 'n nat

val to_int : 'n nat -> int

The call to_int n returns an integer equal to n. This function complexity is O(1).

val of_int : int -> positive_or_null option

Returns a positive or null natural. If the given parameter is stricly negative then None is returned. This function complexity is O(1).

val of_strictly_positive_int : int -> strictly_positive option

Returns a strictly positive natural. If the given parameter is less or equal than zero, then None is returned. This function complexity is O(1).