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-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-eva.core/Eva/Abstract_location/index.html

Module `Eva.Abstract_location`

Signature of abstract memory locations, representing the set of possible memory locations pointed to by an lvalue.

Abstract memory locations of the analysis.

type 'v truth = 'v Abstract_value.truth

module type S = sig ... end

Signature of abstract memory locations.

type 'loc key

module type Leaf = sig ... end

Signature for a leaf module of abstract locations.

type 'l dependencies =

| Leaf : (module Leaf with type location = 'l) -> 'l dependencies
| Node : 'l dependencies * 'r dependencies -> ('l * 'r) dependencies

Eva abstractions are divided between values, locations and domains. Domains depend on locations, and use this type to declare such dependencies. In the standard case, a domain depends on a single location module Loc and uses Leaf (module Loc) to declare this dependency.