package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Builtins management

module Frama_c_builtins : State_builder.Hashtbl with type key = string and type data = Cil_types.varinfo

This module associates the name of a built-in function that might be used during elaboration with the corresponding varinfo. This is done when parsing ${FRAMAC_SHARE}/libc/__fc_builtins.h, which is always performed before processing the actual list of files provided on the command line (see File.init_from_c_files). Actual list of such built-ins is managed in Cabs2cil.

val is_builtin : Cil_types.varinfo -> bool
  • returns

    true if the given variable refers to a Frama-C builtin.

  • since Fluorine-20130401
val is_unused_builtin : Cil_types.varinfo -> bool
  • returns

    true if the given variable refers to a Frama-C builtin that is not used in the current program. Plugins may (and in fact should) hide this builtin from their outputs

val is_special_builtin : string -> bool
  • returns

    true if the given name refers to a special built-in function. A special built-in function can have any number of arguments. It is up to the plug-ins to know what to do with it.

  • since Carbon-20101201
val add_special_builtin : string -> unit

register a new special built-in function

val add_special_builtin_family : (string -> bool) -> unit

register a new family of special built-in functions.

  • since Carbon-20101201
val init_builtins : unit -> unit

initialize the C built-ins. Should be called once per project, after the machine has been set.

module Builtin_functions : State_builder.Hashtbl with type key = string and type data = Cil_types.typ * Cil_types.typ list * bool

A list of the built-in functions for the current compiler (GCC or * MSVC, depending on !msvcMode). Maps the name to the * result and argument types, and whether it is vararg. * Initialized by Cil.initCIL. Do not add builtins directly, use * add_custom_builtin below for that. * * This map replaces gccBuiltins and msvcBuiltins in previous * versions of CIL.

type compiler =
  1. | GCC
  2. | MSVC
  3. | Not_MSVC
val string_of_compiler : compiler -> string
type builtin_template = {
  1. name : string;
  2. compiler : compiler option;
  3. rettype : string;
  4. args : string list;
  5. types : string list option;
  6. variadic : bool;
}
module Builtin_templates : State_builder.Hashtbl with type key = string and type data = builtin_template
val init_gcc_builtin_templates : unit -> unit
val add_custom_builtin : (unit -> string * Cil_types.typ * Cil_types.typ list * bool) -> unit

Register a new builtin. The function will be called after setting the machdep and initializing machine-dependent builtins. Hence, types such Cil.uint16_t might be used if needed.

  • since 23.0-Vanadium
val builtinLoc : Cil_types.location

This is used as the location of the prototypes of builtin functions.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct