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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

doc/frama-c-wp.core/Wp/Context/index.html

Module `Wp.Context`Source

Current Loc

Source

val with_current_loc : 
  Frama_c_kernel.Cil_types.location ->
  ('a -> 'b) ->
  'a ->
  'b

Contextual Values

Sourcetype 'a value

Sourceval create : ?default:'a -> string -> 'a value

Creates a new context with name

Sourceval defined : 'a value -> bool

The current value is defined.

Sourceval get : 'a value -> 'a

Retrieves the current value of the context. Raise an exception if not bound.

Sourceval get_opt : 'a value -> 'a option

Retrieves the current value of the context. Return None if not bound.

Sourceval set : 'a value -> 'a -> unit

Define the current value. Previous one is lost

Sourceval update : 'a value -> ('a -> 'a) -> unit

Modification of the current value

Sourceval bind : 'a value -> 'a -> ('b -> 'c) -> 'b -> 'c

Performs the job with local context bound to local value.

Sourceval free : 'a value -> ('b -> 'c) -> 'b -> 'c

Performs the job with local context cleared.

Sourceval clear : 'a value -> unit

Clear the current value.

Sourceval push : 'a value -> 'a -> 'a option

Sourceval pop : 'a value -> 'a option -> unit

Sourceval name : 'a value -> string

Sourceval register : (unit -> unit) -> unit

Sourceval configure : unit -> unit

Apply global configure hooks, once per project/ast.