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.kernel/Frama_c_kernel/State/index.html

Module `Frama_c_kernel.State`

A state is a project-compliant mutable value.

since Carbon-20101201

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Type declarations

include Datatype.S_with_collections

include Datatype.S

include Datatype.S_no_copy

include Datatype.Ty

type t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val ty : t Type.t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val name : string

Unique name of the datatype.

val descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

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

Pretty print each value in an user-friendly way.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

module Set : Datatype.Set with type elt = t

module Map : Datatype.Map with type key = t

module Hashtbl : Datatype.Hashtbl with type key = t

module type Local = sig ... end

Operations on the local state required for registering a new state via State_builder.Register. The local state is the mutable value which you would like to be project-compliant.

Getters and setters

val get_name : t -> string

Name of a state.

since Carbon-20101201

val set_name : t -> string -> unit

Set the name of the given state.

since Carbon-20101201

val get_unique_name : t -> string

Unique name of a state.

since Carbon-20101201

val unique_name_from_name : string -> string

returns
a fresh unique state name from the given name.

since Nitrogen-20111001

val dummy : t

A dummy state.

since Carbon-20101201

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val dummy_unique_name : string

val is_dummy : t -> bool

returns
true if the given state is dummy.

since Carbon-20101201

exception Unknown

val get : string -> t

returns
the state corresponding to the given unique name.

raises Unknown
if there is no such state.

since Carbon-20101201

val get_descr : t -> Structural_descr.pack

since Carbon-20101201

val add_hook_on_update : t -> (unit -> unit) -> unit

Add an hook which is applied each time the project library changes the local value of the state.

since Nitrogen-20111001

Internals

All this stuff should not be used outside of the Project library.

type state_on_disk = {

on_disk_value : Obj.t;
on_disk_computed : bool;
on_disk_saved : bool;
on_disk_digest : Digest.t;

}

since Carbon-20101201

type private_ops = private {

descr : Structural_descr.pack;
create : Project_skeleton.project -> unit;
remove : Project_skeleton.project -> unit;
clear : Project_skeleton.project -> unit;
clear_some_projects : (Project_skeleton.project -> bool) -> Project_skeleton.project -> bool;
copy : Project_skeleton.project -> Project_skeleton.project -> unit;
commit : Project_skeleton.project -> unit;
update : Project_skeleton.project -> unit;
on_update : (unit -> unit) -> unit;
clean : unit -> unit;
serialize : Project_skeleton.project -> state_on_disk;
unserialize : Project_skeleton.project -> state_on_disk -> unit;
(*
- raises Incompatible_datatype
  if state_on_disk is not compatible with the datatype expected by Frama-C's state
*)

}

since Carbon-20101201

exception Incompatible_datatype of string

val dummy_state_on_disk : state_on_disk

val private_ops : t -> private_ops

since Carbon-20101201

State generators

val create : 
  descr:Structural_descr.pack ->
  create:(Project_skeleton.project -> unit) ->
  remove:(Project_skeleton.project -> unit) ->
  clear:(Project_skeleton.project -> unit) ->
  clear_some_projects:
    ((Project_skeleton.project -> bool) -> Project_skeleton.project -> bool) ->
  copy:(Project_skeleton.project -> Project_skeleton.project -> unit) ->
  commit:(Project_skeleton.project -> unit) ->
  update:(Project_skeleton.project -> unit) ->
  on_update:((unit -> unit) -> unit) ->
  clean:(unit -> unit) ->
  serialize:(Project_skeleton.project -> state_on_disk) ->
  unserialize:(Project_skeleton.project -> state_on_disk -> unit) ->
  unique_name:string ->
  name:string ->
  t

since Carbon-20101201

val delete : t -> unit

since Carbon-20101201

On This Page

Type declarations
Getters and setters
Internals
1. State generators