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-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Logic_typing/Make/argument-1-C/index.html

Parameter `Make.C`

val is_loop : unit -> bool

whether the annotation we want to type is contained in a loop. Only useful when creating objects of type code_annotation.

val anonCompFieldName : string

val conditionalConversion : Cil_types.typ -> Cil_types.typ -> Cil_types.typ

val find_macro : string -> Logic_ptree.lexpr

val find_var : ?label:string -> string -> Cil_types.logic_var

see corresponding field in Logic_typing.typing_context.

val find_enum_tag : string -> Cil_types.exp * Cil_types.typ

val find_type : type_namespace -> string -> Cil_types.typ

val find_comp_field : Cil_types.compinfo -> string -> Cil_types.offset

val find_label : string -> Cil_types.stmt ref

val remove_logic_function : string -> unit

val remove_logic_info : Cil_types.logic_info -> unit

val remove_logic_type : string -> unit

val remove_logic_ctor : string -> unit

val add_logic_function : Cil_types.logic_info -> unit

val add_logic_type : string -> Cil_types.logic_type_info -> unit

val add_logic_ctor : string -> Cil_types.logic_ctor_info -> unit

val find_all_logic_functions : string -> Cil_types.logic_info list

val find_logic_type : string -> Cil_types.logic_type_info

val find_logic_ctor : string -> Cil_types.logic_ctor_info

val integral_cast : Cil_types.typ -> Cil_types.term -> Cil_types.term

What to do when we have a term of type Integer in a context expecting a C integral type.

raises Failure
to reject such conversion

since Nitrogen-20111001

val error : 
  Cil_types.location ->
  ('a, Format.formatter, unit, 'b) format4 ->
  'a

raises an error at the given location and with the given message.

since Magnesium-20151001

val on_error : 
  ('a -> 'b) ->
  ((Cil_types.location * string) -> unit) ->
  'a ->
  'b

see Logic_typing.typing_context.