LogicBuiltins (frama-c-wp.Wp.LogicBuiltins)

type category = Lang.lfun Qed.Logic.category

type kind =

| B
(*
boolean
*)
| Z
(*
integer
*)
| R
(*
real
*)
| I of Ctypes.c_int
(*
C-ints
*)
| F of Ctypes.c_float
(*
C-floats
*)
| 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.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

val find_lib : Frama_c_kernel.Filepath.t -> Frama_c_kernel.Filepath.t

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 =

| ACSLDEF
| LFUN of Lang.lfun
| HACK of Lang.F.term list -> Lang.F.term

val logic : Frama_c_kernel.Cil_types.logic_info -> builtin

val ctor : Frama_c_kernel.Cil_types.logic_ctor_info -> builtin

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