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-30.0-Zinc.tar.gz

sha256=3ac0f995261ec829a7bd042bf70fc29ac6379029eb9df30bcc044748eb4d2a56

doc/frama-c-region.core/Region/index.html

Module `Region`Source

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.

Sourcetype map

Sourcetype node

Sourceval get_map : Frama_c_kernel.Cil_types.kernel_function -> map

Sourceval get_id : map -> node -> int

Sourceval get_node : map -> int -> node

Sourceval node : map -> node -> node

Normalize node

Sourceval nodes : map -> node list -> node list

Normalize set of nodes

Sourceval equal : map -> node -> node -> bool

Nodes are in the same region

Sourceval included : map -> node -> node -> bool

First belongs to last

Sourceval separated : map -> node -> node -> bool

Nodes can not be aliased

Sourceval cvar : map -> Frama_c_kernel.Cil_types.varinfo -> node

Sourceval field : map -> node -> Frama_c_kernel.Cil_types.fieldinfo -> node

Sourceval index : map -> node -> Frama_c_kernel.Cil_types.typ -> node

Sourceval lval : map -> Frama_c_kernel.Cil_types.lval -> node

Sourceval exp : map -> Frama_c_kernel.Cil_types.exp -> node option

Sourceval points_to : map -> node -> node option

Sourceval pointed_by : map -> node -> node list

Sourceval parents : map -> node -> node list

Sourceval roots : map -> node -> Frama_c_kernel.Cil_types.varinfo list

Sourceval iter : map -> (node -> unit) -> unit

Iter over all regions

Sourceval reads : map -> node -> Frama_c_kernel.Cil_types.typ list

Sourceval writes : map -> node -> Frama_c_kernel.Cil_types.typ list

Sourceval shifts : map -> node -> Frama_c_kernel.Cil_types.typ list