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/Lang/index.html

Module `Wp.Lang`Source

Low-Level Logic Terms and Predicates

Logic Language based on Qed

Library

Sourcetype library = string

Naming - Unique identifiers

Sourceval comp_id : Frama_c_kernel.Cil_types.compinfo -> string

Sourceval comp_init_id : Frama_c_kernel.Cil_types.compinfo -> string

Sourceval field_id : Frama_c_kernel.Cil_types.fieldinfo -> string

Sourceval field_init_id : Frama_c_kernel.Cil_types.fieldinfo -> string

Sourceval type_id : Frama_c_kernel.Cil_types.logic_type_info -> string

Sourceval logic_id : Frama_c_kernel.Cil_types.logic_info -> string

Sourceval ctor_id : Frama_c_kernel.Cil_types.logic_ctor_info -> string

Sourceval lemma_id : string -> string

Symbols

Sourcetype datakind =

| KValue
| KInit

Sourcetype adt = private

| Mtype of mdt
(*
External type
*)
| Mrecord of mdt * fields
(*
External record-type
*)
| Atype of Frama_c_kernel.Cil_types.logic_type_info
(*
Logic Type
*)
| Comp of Frama_c_kernel.Cil_types.compinfo * datakind
(*
C-code struct or union
*)

A type is never registered in a Definition.t

Sourceand mdt = string extern

name to print to the provers

Sourceand 'a extern = {

ext_id : int;
ext_link : 'a;
ext_library : library;
(*
a library which it depends on
*)
ext_debug : string;
(*
just for printing during debugging
*)

}

Sourceand fields = {

mutable fields : field list;

}

Sourceand field = private

| Mfield of mdt * fields * string * tau
| Cfield of Frama_c_kernel.Cil_types.fieldinfo * datakind

Sourceand tau = (field, adt) Qed.Logic.datatype

Sourcetype t_builtin =

| E_mdt of mdt
| E_poly of tau list -> tau

Sourcetype lfun = private

| ACSL of Frama_c_kernel.Cil_types.logic_info
(*
Registered in Definition.t, only
*)
| CTOR of Frama_c_kernel.Cil_types.logic_ctor_info
(*
Not registered in Definition.t directly converted/printed
*)
| FUN of lsymbol
(*
External or Generated logic symbol
*)

Sourceand lsymbol = {

m_category : lfun Qed.Logic.category;
m_params : Qed.Logic.sort list;
m_result : Qed.Logic.sort;
m_typeof : tau option list -> tau;
m_source : source;
m_coloring : bool;

}

Sourceand source =

| Generated of WpContext.context option * string
| Extern of Qed.Engine.link extern

Sourceval mem_builtin_type : name:string -> bool

Sourceval is_builtin : Frama_c_kernel.Cil_types.logic_type_info -> bool

Sourceval is_builtin_type : name:string -> tau -> bool

Sourceval get_builtin_type : name:string -> adt

Sourceval datatype : library:string -> string -> adt

Sourceval record : link:string -> library:string -> (string * tau) list -> adt

Sourceval comp : Frama_c_kernel.Cil_types.compinfo -> adt

Sourceval comp_init : Frama_c_kernel.Cil_types.compinfo -> adt

Sourceval cfield : ?kind:datakind -> Frama_c_kernel.Cil_types.fieldinfo -> field

Sourceval field : adt -> string -> field

Sourceval fields_of_adt : adt -> field list

Sourceval fields_of_tau : tau -> field list

Sourceval fields_of_field : field -> field list

Sourceval atype : Frama_c_kernel.Cil_types.logic_type_info -> tau list -> tau

Sourceval adt : Frama_c_kernel.Cil_types.logic_type_info -> adt

Must not be a builtin

Sourcetype balance =

| Nary
| Left
| Right

Sourceval on_lfun : (lfun -> unit) -> unit

Sourceval on_field : (field -> unit) -> unit

Sourceval acsl : Frama_c_kernel.Cil_types.logic_info -> lfun

Sourceval ctor : Frama_c_kernel.Cil_types.logic_ctor_info -> lfun

Source

val extern_s : 
  library:library ->
  ?link:Qed.Engine.link ->
  ?category:lfun Qed.Logic.category ->
  ?params:Qed.Logic.sort list ->
  ?sort:Qed.Logic.sort ->
  ?result:tau ->
  ?coloring:bool ->
  ?typecheck:(tau option list -> tau) ->
  string ->
  lfun

Source

val extern_f : 
  library:library ->
  ?link:Qed.Engine.link ->
  ?balance:balance ->
  ?category:lfun Qed.Logic.category ->
  ?params:Qed.Logic.sort list ->
  ?sort:Qed.Logic.sort ->
  ?result:tau ->
  ?coloring:bool ->
  ?typecheck:(tau option list -> tau) ->
  ('a, Format.formatter, unit, lfun) format4 ->
  'a

balance just give a default when link is not specified

Source

val extern_p : 
  library:library ->
  ?bool:string ->
  ?prop:string ->
  ?link:Qed.Engine.link ->
  ?params:Qed.Logic.sort list ->
  ?coloring:bool ->
  unit ->
  lfun

Source

val extern_fp : 
  library:library ->
  ?params:Qed.Logic.sort list ->
  ?link:string ->
  ?coloring:bool ->
  string ->
  lfun

Source

val generated_f : 
  ?context:bool ->
  ?category:lfun Qed.Logic.category ->
  ?params:Qed.Logic.sort list ->
  ?sort:Qed.Logic.sort ->
  ?result:tau ->
  ?coloring:bool ->
  ('a, Format.formatter, unit, lfun) format4 ->
  'a

Sourceval generated_p : ?context:bool -> ?coloring:bool -> string -> lfun

Sourceval extern_t : string -> link:string -> library:library -> mdt

Sorting and Typing

Sourceval tau_of_object : Ctypes.c_object -> tau

Sourceval tau_of_ctype : Frama_c_kernel.Cil_types.typ -> tau

Sourceval tau_of_ltype : Frama_c_kernel.Cil_types.logic_type -> tau

Sourceval tau_of_return : Frama_c_kernel.Cil_types.logic_type option -> tau

Sourceval tau_of_lfun : lfun -> tau option list -> tau

Sourceval tau_of_field : field -> tau

Sourceval tau_of_record : field -> tau

Sourceval init_of_object : Ctypes.c_object -> tau

Sourceval init_of_ctype : Frama_c_kernel.Cil_types.typ -> tau

Sourceval t_int : tau

Sourceval t_real : tau

Sourceval t_bool : tau

Sourceval t_prop : tau

Sourceval t_addr : unit -> tau

Sourceval t_comp : Frama_c_kernel.Cil_types.compinfo -> tau

Sourceval t_init : Frama_c_kernel.Cil_types.compinfo -> tau

Sourceval t_float : Ctypes.c_float -> tau

Sourceval t_array : tau -> tau

Sourceval t_farray : tau -> tau -> tau

Sourceval t_datatype : adt -> tau list -> tau

Sourceval t_matrix : tau -> int -> tau

Sourceval pointer : tau Context.value

type of pointers

Sourceval floats : (Ctypes.c_float -> tau) Context.value

type of floats

Sourceval poly : string list Context.value

polymorphism

Sourceval builtin_types : (string -> t_builtin) Context.value

Sourceval parameters : (lfun -> Qed.Logic.sort list) -> unit

definitions

Sourceval name_of_lfun : lfun -> string

Sourceval name_of_field : field -> string

Sourceval context_of_lfun : lfun -> WpContext.context option

LFuns are unique by name and context

Sourceval is_coloring_lfun : lfun -> bool

Logic Formulae

Sourcemodule ADT : Qed.Logic.Data with type t = adt

Sourcemodule Field : Qed.Logic.Field with type t = field

Sourcemodule Fun : Qed.Logic.Function with type t = lfun

Sourceclass virtual idprinting : object ... end

Sourcemodule F : sig ... end

Sourcemodule N : sig ... end

simpler notation for writing F.term and F.pred

Fresh Variables and Constraints

Sourcetype gamma

Sourceval new_pool : ?copy:F.pool -> ?vars:F.Vars.t -> unit -> F.pool

Sourceval new_gamma : ?copy:gamma -> unit -> gamma

Source

val local : 
  ?pool:F.pool ->
  ?vars:F.Vars.t ->
  ?gamma:gamma ->
  ('a -> 'b) ->
  'a ->
  'b

Sourceval freshvar : ?basename:string -> F.tau -> F.var

Sourceval freshen : F.var -> F.var

Sourceval assume : F.pred -> unit

Sourceval without_assume : ('a -> 'b) -> 'a -> 'b

Sourceval hypotheses : gamma -> F.pred list

Sourceval get_pool : unit -> F.pool

Sourceval get_gamma : unit -> gamma

Sourceval has_gamma : unit -> bool

Sourceval get_hypotheses : unit -> F.pred list

Sourceval filter_hypotheses : F.var list -> F.pred list

Substitutions

Sourceval sigma : unit -> F.sigma

uses current pool

Sourceval alpha : unit -> F.sigma

freshen all variables

Sourceval subst : F.var list -> F.term list -> F.sigma

replace variables

Sourceval e_subst : (F.term -> F.term) -> F.term -> F.term

uses current pool

Sourceval p_subst : (F.term -> F.term) -> F.pred -> F.pred

uses current pool

Simplifiers

Sourceexception Contradiction

Sourceval is_literal : F.term -> bool

Sourceval iter_consequence_literals : (F.term -> unit) -> F.term -> unit

iter_consequence_literals assume_from_litteral hypothesis applies the function assume_from_litteral on literals that are a consequence of the hypothesis (i.e. in the hypothesis not (A && (B || C) ==> D), only A and not D are considered as consequence literals).

Sourceclass type simplifier = object ... end

Sourcemodule For_export : sig ... end

For why3_api but circular dependency

On This Page

Library
Naming - Unique identifiers
Symbols
Sorting and Typing
Logic Formulae
Fresh Variables and Constraints
Substitutions
Simplifiers

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module Wp.LangSource

Library

Naming - Unique identifiers

Symbols

Sorting and Typing

Logic Formulae

Fresh Variables and Constraints

Substitutions

Simplifiers

Module `Wp.Lang`Source