package frama-c

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

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.

type t

Type of the state to register.

val create : unit -> t

How to create a new fresh state which must be equal to the initial state: that is, if you never change the state, create () and get () must be equal (see invariant 1 below).

val clear : t -> unit

How to clear a state. After clearing, the state should be observationally the same that after its creation (see invariant 2 below).

val get : unit -> t

How to access to the current state. Be aware of invariants 3 and 4 below.

val set : t -> unit

How to change the current state. Be aware of invariants 3 and 4 below.

The four following invariants must hold.

  1. create () returns a fresh value
  2. forall (p:t) copy p returns a fresh value
  3. forall (p:t), create () = (clear p; set p; get ())
  4. forall (p1:t),(p2:t) such that p1 != p2, (set p1; get ()) != s2
val clear_some_projects : (Project_skeleton.t -> bool) -> t -> bool

clear_if_project f x must clear any value v of type project of x such that f v is true. Of course, if the type t does not contain any object of type project, this function should do nothing and safely returns fun _ -> false.

  • returns

    true iff at least one element of x has been cleared.

  • since Boron-20100401
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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