package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
type kind =
  1. | Z
    (*

    integer

    *)
  2. | R
    (*

    real

    *)
  3. | I of Ctypes.c_int
    (*

    C-ints

    *)
  4. | F of Ctypes.c_float
    (*

    C-floats

    *)
  5. | A
    (*

    Abstract Data

    *)
val kind_of_tau : Lang.tau -> kind
val add_builtin : string -> kind list -> Lang.lfun -> unit

Add a new builtin. This builtin will be shared with all created drivers

type driver
val driver : driver Context.value
val new_driver : id:string -> ?base:driver -> ?descr:string -> ?includes:Frama_c_kernel.Filepath.Normalized.t list -> ?configure:(unit -> unit) -> unit -> driver

Creates a configured driver from an existing one. Default:

  • base: builtin WP driver
  • descr: id
  • includes:
  • configure: No-Op The configure is the only operation allowed to modify the content of the newly created driver. Except during static initialization of builtin driver.
val id : driver -> string
val descr : driver -> string
val is_default : driver -> bool
val compare : driver -> driver -> int

find a file in the includes of the current drivers

val dependencies : string -> string list

Of external theories. Raises Not_found if undefined

val add_library : string -> string list -> unit

Add a new library or update the dependencies of an existing one

val add_alias : source:Frama_c_kernel.Filepath.position -> string -> kind list -> alias:string -> unit -> unit
val add_type : ?source:Frama_c_kernel.Filepath.position -> string -> library:string -> ?link:string -> unit -> unit
val add_ctor : source:Frama_c_kernel.Filepath.position -> string -> kind list -> library:string -> link:Qed.Engine.link -> unit -> unit
val add_logic : source:Frama_c_kernel.Filepath.position -> kind -> string -> kind list -> library:string -> ?category:category -> link:Qed.Engine.link -> unit -> unit
val add_predicate : source:Frama_c_kernel.Filepath.position -> string -> kind list -> library:string -> link:string -> unit -> unit
val add_option : driver_dir:string -> string -> string -> library:string -> string -> unit

add a value to an option (group, name)

val set_option : driver_dir:string -> string -> string -> library:string -> string -> unit

reset and add a value to an option (group, name)

type doption
type sanitizer = driver_dir:string -> string -> string
val create_option : sanitizer:sanitizer -> string -> string -> doption

add_option_sanitizer ~driver_dir group name add a sanitizer for group group and option name

val get_option : doption -> library:string -> string list

return the values of option (group, name), return the empty list if not set

type builtin =
  1. | ACSLDEF
  2. | LFUN of Lang.lfun
  3. | HACK of Lang.F.term list -> Lang.F.term
val constant : string -> builtin
val lookup : string -> kind list -> builtin
val hack : string -> (Lang.F.term list -> Lang.F.term) -> unit

Replace a logic definition or predicate by a built-in function. The LogicSemantics compilers will replace `Pcall` and `Tcall` instances of this symbol with the provided Qed function on terms.

val hack_type : string -> (Lang.F.tau list -> Lang.F.tau) -> unit

Replace a logic type definition or predicate by a built-in type.

val dump : unit -> 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