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

Module `Wp.WpContext`Source

Model Registration

Sourcetype model

Sourcetype scope =

| Global
| Kf of Frama_c_kernel.Kernel_function.t

Sourcetype rollback = unit -> unit

Sourcetype hypotheses = MemoryContext.partition -> MemoryContext.partition

Source

val register : 
  id:string ->
  ?descr:string ->
  configure:(unit -> rollback) ->
  ?hypotheses:hypotheses ->
  unit ->
  model

Model registration. The model is identified by id and described by descr (that defaults to id). The configure function is called on WpContext.on_context call, it must prepare and set the different Context.values related to the model. It must return the function that allows to rollback on the original state. The hypotheses function must return the hypotheses made by the model.

Sourceval get_descr : model -> string

Sourceval get_emitter : model -> Frama_c_kernel.Emitter.t

Source

val compute_hypotheses : 
  model ->
  Frama_c_kernel.Kernel_function.t ->
  MemoryContext.partition

Sourcetype context = model * scope

Sourcetype t = context

Sourcemodule S : sig ... end

Sourcemodule MODEL : sig ... end

Sourcemodule SCOPE : sig ... end

Sourcemodule MINDEX : Hashtbl.S with type key = model

Sourceval is_defined : unit -> bool

Sourceval on_context : context -> ('a -> 'b) -> 'a -> 'b

Sourceval get_model : unit -> model

Sourceval get_ident : unit -> string

Sourceval get_scope : unit -> scope

Sourceval get_context : unit -> context

Sourceval directory : unit -> Frama_c_kernel.Datatype.Filepath.t

Current model in "-wp-out" directory

Sourcemodule type Entries = sig ... end

Sourcemodule type Registry = sig ... end

Sourcemodule Index (E : Entries) : Registry with module E = E

projectified, depend on the model, not serialized

Sourcemodule Static (E : Entries) : Registry with module E = E

projectified, independent from the model, not serialized

Sourcemodule type Key = sig ... end

Sourcemodule type Data = sig ... end

Sourcemodule type IData = sig ... end

Sourcemodule type Generator = sig ... end

Source

module Generator
  (K : Key)
  (D : Data with type key = K.t) : 
  Generator with type key = D.key and type data = D.data

projectified, depend on the model, not serialized

Source

module StaticGenerator
  (K : Key)
  (D : Data with type key = K.t) : 
  Generator with type key = D.key and type data = D.data

projectified, independent from the model, not serialized

Source

module GeneratorID
  (K : Key)
  (D : IData with type key = K.t) : 
  Generator with type key = D.key and type data = D.data

projectified, depend on the model, not serialized

Source

module StaticGeneratorID
  (K : Key)
  (D : IData with type key = K.t) : 
  Generator with type key = D.key and type data = D.data

projectified, independent from the model, not serialized

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Wp.WpContextSource

Module `Wp.WpContext`Source