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 (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c.kernel/Frama_c_kernel/Cil_builtins/index.html

Module `Frama_c_kernel.Cil_builtins`

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 has_fc_builtin_attr or is_special_builtin are true.

before 29.0-Copper
Only check for has_fc_builtin_attr.

since Fluorine-20130401

val has_fc_builtin_attr : Cil_types.varinfo -> bool

returns
true if the given variable has a FC_BUILTIN attribute

since 29.0-Copper

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

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

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 !Machine.msvcMode). Maps the name to the result and argument types, and whether it is vararg. Initialized by Machine.init. Do not add builtins directly, use add_custom_builtin below for that.

type compiler =

| GCC
| MSVC
| Not_MSVC

val string_of_compiler : compiler -> string

type builtin_template = {

name : string;
compiler : compiler option;
rettype : string;
args : string list;
types : string list option;
variadic : bool;

}

module Builtin_templates : 
  State_builder.Hashtbl with type key = string and type data = builtin_template

module Gcc_builtin_templates_loaded : State_builder.Ref with type data = bool

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.

On This Page

Builtins management