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

Module `Eva.Simple_memory`

Build a domain upon a value abstraction with a very simple memory model for scalar non-volatile variables.

Simple memory abstraction for scalar non-volatile variables, built upon a value abstraction. Basically a map from variable to values.

type 'value builtin = 'value list -> 'value Eval.or_bottom

A builtin is an ocaml function for the interpretation of a whole C function: it takes the list of value arguments, and returns the result (that can be bottom).

type widen_hint = Frama_c_kernel.Z.Set.t * Frama_c_kernel.Datatype.Float.Set.t

Set of relevant thresholds for the widening.

module type Value = sig ... end

Abstraction of the values variables are mapped to.

module type S = sig ... end

Signature of a simple memory abstraction for scalar variables.

module Make_Memory (_ : sig ... end) (Value : Value) : sig ... end

module Make_Domain (_ : sig ... end) (Value : Value) : sig ... end