package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/LogicBuiltins/index.html

Module `Wp.LogicBuiltins`Source

Sourcetype category = Lang.lfun Qed.Logic.category

Sourcetype kind =

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

Source

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.

Sourceval id : driver -> string

Sourceval descr : driver -> string

Sourceval is_default : driver -> bool

Sourceval compare : driver -> driver -> int

Source

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

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

Source

val add_alias : 
  source:Frama_c_kernel.Filepath.position ->
  string ->
  kind list ->
  alias:string ->
  unit ->
  unit

Source

val add_type : 
  ?source:Frama_c_kernel.Filepath.position ->
  string ->
  library:string ->
  ?link:string ->
  unit ->
  unit

Source

val add_ctor : 
  source:Frama_c_kernel.Filepath.position ->
  string ->
  kind list ->
  library:string ->
  link:Qed.Engine.link ->
  unit ->
  unit

Source

val add_logic : 
  source:Frama_c_kernel.Filepath.position ->
  kind ->
  string ->
  kind list ->
  library:string ->
  ?category:category ->
  link:Qed.Engine.link ->
  unit ->
  unit

Source

val add_predicate : 
  source:Frama_c_kernel.Filepath.position ->
  string ->
  kind list ->
  library:string ->
  link:string ->
  unit ->
  unit

Source

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

add a value to an option (group, name)

Source

val 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 =

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

Sourceval logic : Frama_c_kernel.Cil_types.logic_info -> builtin

Sourceval ctor : Frama_c_kernel.Cil_types.logic_ctor_info -> builtin

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

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/LogicBuiltins/index.html

Module Wp.LogicBuiltinsSource

Module `Wp.LogicBuiltins`Source