Frama-C:
Plug-ins:
Libraries:

Frama-C API - LogicBuiltins

type kind =
  1. | B
    (*

    boolean

    *)
  2. | Z
    (*

    integer

    *)
  3. | R
    (*

    real

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

    C-ints

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

    C-floats

    *)
  6. | 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.

val add_builtin_type : string -> Lang.adt -> unit

Add a new builtin type. Must be an extern or imported type. 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