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 (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/MemVal/Eva/index.html

Module `MemVal.Eva`Source

The glue between WP and EVA. *

Sourceval configure : unit -> WpContext.rollback

Sourceval datatype : string

Sourcemodule State : State

Sourcetype t

abstract value *

Sourcetype state = State.t

Sourceval null : t

Sourceval literal : eid:int -> Cstring.cst -> int * t

literal eid cstr returns the pair of base identifier and abstract value corresponding to the concrete string constant cstr of unique expression identifier eid. eid should be a valid identifier for cstr. *

Sourceval cvar : Frama_c_kernel.Cil_types.varinfo -> t

cvar x returns the abstract value corresponding to &x. *

Sourceval field : t -> Frama_c_kernel.Cil_types.fieldinfo -> t

field v fd returns the value obtained by access to field fd from v. *

Sourceval shift : t -> Ctypes.c_object -> Lang.F.term -> t

shift v obj k returns the value obtained by access at an index k with type obj from v. *

Sourceval base_addr : t -> t

base_addr v returns the value corresponding to the base address of v. *

Sourceval load : state -> t -> Ctypes.c_object -> t

load s v obj returns the value at the location given by v with type obj within the state s. *

Sourceval domain : t -> Frama_c_kernel.Base.t list

domain v returns a list of all possible concrete bases of v. *

Sourceval offset : t -> Lang.F.term -> Lang.F.pred

offset v returns a function which when applied with a term returns a predicate over v's offset.

Sourceval pretty : Format.formatter -> t -> unit