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