package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

The glue between WP and EVA. *

val configure : unit -> WpContext.rollback
val datatype : string
module State : State
type t

abstract value *

type state = State.t
val null : t
val 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. *

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

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

val 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. *

val base_addr : t -> t

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

val 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. *

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

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

val 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.

val pretty : Format.formatter -> t -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct