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/Simpler_domains/index.html

Module `Eva.Simpler_domains`

Simplified interfaces for abstract domains. Complete abstract domains can be built from these interfaces through the functors in Domain_builder.

Simplified interfaces for abstract domains. Complete abstract domains can be built from these interfaces through the functors in Domain_builder. More documentation can be found on the complete interface of abstract domains, in Abstract_domain.

type simple_argument = {

formal : Frama_c_kernel.Cil_types.varinfo;
concrete : Eval.exp;

}

Both the formal argument of a called function and the concrete argument at a call site.

type simple_call = {

kf : Frama_c_kernel.Cil_types.kernel_function;
arguments : simple_argument list;
rest : Eval.exp list;
return : Frama_c_kernel.Cil_types.varinfo option;

}

Simple information about a function call.

module type Minimal = sig ... end

Simplest interface for an abstract domain. No exchange of information with the other abstractions of Eva.

module type Minimal_with_datatype = sig ... end

The simplest interface of domains, equipped with a frama-c datatype.

type cvalue_valuation = {

find : Eval.exp -> Frama_c_kernel.Cvalue.V.t Eval.flagged_value Eval.or_top;
find_loc : Eval.lval -> Frama_c_kernel.Precise_locs.precise_location Eval.or_top;

}

A simpler functional interface for valuations.

type precise_loc = Frama_c_kernel.Precise_locs.precise_location

type cvalue = Frama_c_kernel.Cvalue.V.t

module type Simple_Cvalue = sig ... end

A simple interface allowing the abstract domain to use the value and location abstractions computed by the other domains. Only the Cvalue.V and the the Precise_locs abstractions are available in this interface, on the transfer functions for assignment, assumption and at the call sites. On the other hand, the abstract domain cannot assist the computation of these value and location abstractions. The communication is thus unidirectional, from other domains to these simpler domains.