package frama-c

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

Module Wp.LogicBuiltinsSource

Sourcetype 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

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

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

Sourcetype driver
Sourceval 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.
Sourceval id : driver -> string
Sourceval descr : driver -> string
Sourceval is_default : driver -> bool
Sourceval compare : driver -> driver -> int

find a file in the includes of the current drivers

Sourceval dependencies : string -> string list

Of external theories. Raises Not_found if undefined

Sourceval add_library : string -> string list -> unit

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

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

add a value to an option (group, name)

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

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

Sourcetype doption
Sourcetype sanitizer = driver_dir:string -> string -> string
Sourceval create_option : sanitizer:sanitizer -> string -> string -> doption

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

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

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

Sourcetype builtin =
  1. | ACSLDEF
  2. | LFUN of Lang.lfun
  3. | HACK of Lang.F.term list -> Lang.F.term
Sourceval constant : string -> builtin
Sourceval lookup : string -> kind list -> builtin
Sourceval 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.

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

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

Sourceval 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