package frama-clang

You can search for identifiers within the package.

in-package search v0.2.0

frama-clang.core
- Clang
  - Class
  - Convert
  - Convert_acsl
  - Convert_env
  - Convert_link
  - Cxx_utils
  - Fclang_datatype
    
    Access_kind
    
    Qual_type
    
    Hashtbl
    
    Key
    
    Make
    
    Data
    
    Map
    
    Key
    
    Make
    
    Data
    
    Set
    
    Qualified_name
    
    Hashtbl
    
    Key
    
    Make
    
    Data
    
    Map
    
    Key
    
    Make
    
    Data
    
    Set
    
    Template_parameter
    
    Hashtbl
    
    Key
    
    Make
    
    Data
    
    Map
    
    Key
    
    Make
    
    Data
    
    Set
    
    Vkind
  - Frama_Clang
  - Frama_Clang_option
    
    C_std_headers
    
    Datatype
    
    Clang_command
    
    Datatype
    
    Clang_extra_args
    
    As_string
    
    Datatype
    
    Category
    
    Datatype
    
    Config
    
    Cxx_std_headers
    
    Datatype
    
    Cxx_virtual_bare_methods_in_clang
    
    Datatype
    
    Debug
    
    Datatype
    
    ParseableOutput
    
    Datatype
    
    Session
    
    Share
    
    Std_include
    
    Datatype
    
    Unmangling
    
    Datatype
    
    Verbose
    
    Datatype
  - Frama_Clang_register
  - Generate_spec
  - Intermediate_format
  - Intermediate_format_parser
  - Mangling
  - Reorder_defs

Legend:
Library
Module
Module type
Parameter
Class
Class type

Elements of specification generated from the C++ conversion itself.

val add_contract : 
  env:Convert_env.env ->
  kind:Intermediate_format.funkind ->
  return_type:Intermediate_format.qual_type ->
  args:Intermediate_format.arg_decl list ->
  variadic:bool ->
  implicit:bool ->
  extern_c:bool ->
  (Frama_c_kernel.Logic_ptree.spec * Frama_c_kernel.Cabs.cabsloc) option ->
  (Frama_c_kernel.Logic_ptree.spec * Frama_c_kernel.Cabs.cabsloc) option

adds contract elements to the default behavior of the given spec related to the corresponding signature elements.