package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Edit opam file Versions (30)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-33.0-Arsenic.tar.gz

sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8

doc/frama-c.kernel/Frama_c_kernel/Box/Make/index.html

Module `Box.Make`

This module provides a representation of closed boxes in a classical vector space over a field 𝕂.

Parameters

module K : Field.S

Signature

type 'n t = {

center : 'n Linear.Space(K).vector;
radius : 'n Linear.Space(K).vector;

}

Boxes are represented as a center and a radius. The radius components are always all positives.

val make : 
  'n Nat.succ Linear.Space(K).vector ->
  'n Nat.succ Linear.Space(K).vector ->
  'n Nat.succ t

The call make center radius returns a box of center center and of radius abs radius, with abs the componentwise absolute value on vectors as defined in Linear.

val point : 'n Nat.succ Linear.Space(K).vector -> 'n Nat.succ t

The call point center returns a box of radius zero and of center center, i.e a point in the vector space.

val zero : 'n Nat.succ Nat.nat -> 'n Nat.succ t

The call zero n returns the point zero in a n dimensional vector space.

val pretty : 'n Nat.succ t Pretty_utils.formatter

Pretty printer.

val bounds : 'n t -> 'n Linear.Space(K).vector * 'n Linear.Space(K).vector

Boxes can also be seen as a collection of intervals. The call bounds b returns thus the bounds in each dimension of the closed space defined by b. The lower b (resp. upper b) function returns only the lower bounds (resp. upper bounds).

val lower : 'n t -> 'n Linear.Space(K).vector

val upper : 'n t -> 'n Linear.Space(K).vector

val is_included : 'n t -> 'n t -> bool

The call is_included l r returns true if and only if all points in the box l are also in the box r.

val (+) : 'n t -> 'n t -> 'n t

Minkowsky sum of two boxes, i.e $l + r$ is the box $z$ such as $\forall x \in l, y \in r, x + y \in z$ .