package frama-c

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

Interface for the Region plug-in.

Each function is assigned a region map. Areas in the map represents l-values or, more generally, class of nodes. Regions are classes equivalences of nodes that represents a collection of addresses (at some program point).

Regions can be subdivided into sub-regions. Hence, given two regions, either one is included into the other, or they are separated. Hence, given two l-values, if their associated regions are separated, then they can not be aliased.

Nodes are elementary elements of a region map. Variables maps to nodes, and one can move to one node to another by struct or union field or array element. Two disting nodes might belong to the same region. However, it is possible to normalize nodes and obtain a unique identifier for all nodes in a region.

type map
type node
val get_id : map -> node -> int
val get_node : map -> int -> node
val node : map -> node -> node

Normalize node

val nodes : map -> node list -> node list

Normalize set of nodes

val equal : map -> node -> node -> bool

Nodes are in the same region

val included : map -> node -> node -> bool

First belongs to last

val separated : map -> node -> node -> bool

Nodes can not be aliased

val exp : map -> Frama_c_kernel.Cil_types.exp -> node option
val points_to : map -> node -> node option
val pointed_by : map -> node -> node list
val parents : map -> node -> node list
val iter : map -> (node -> unit) -> unit

Iter over all regions

val reads : map -> node -> Frama_c_kernel.Cil_types.typ list
val writes : map -> node -> Frama_c_kernel.Cil_types.typ list
val shifts : map -> node -> Frama_c_kernel.Cil_types.typ list
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