package frama-c

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

Parameters

Signature

include module type of Exp with type ('v, 's) typ = ('v, 's) Type.typ and type const' = Exp.const' and type var' = Exp.var' and type lval' = Exp.lval' and type exp' = Exp.exp' and type init' = Exp.init' and type label = Exp.label
include module type of Type with type ('v, 's) typ = ('v, 's) Type.typ
exception NotACType
type ('v, 's) typ = ('v, 's) Type.typ
val of_ltyp : Cil_types.logic_type -> (unit, unit) typ
val integer : (unit, unit) typ
val real : (unit, unit) typ
val of_ctyp : Cil_types.typ -> ('v, 'v) typ
val void : ('v, 'v) typ
val bool : ('v, 'v) typ
val char : ('v, 'v) typ
val schar : ('v, 'v) typ
val uchar : ('v, 'v) typ
val int : ('v, 'v) typ
val unit : ('v, 'v) typ
val short : ('v, 'v) typ
val ushort : ('v, 'v) typ
val long : ('v, 'v) typ
val ulong : ('v, 'v) typ
val longlong : ('v, 'v) typ
val ulonglong : ('v, 'v) typ
val float : ('v, 'v) typ
val double : ('v, 'v) typ
val longdouble : ('v, 'v) typ
val ptr : ('v, 's) typ -> ('v, 'v) typ
val array : ?size:int -> ('v, 's) typ -> ('v, 's list) typ
val structure : Cil_types.compinfo -> (Cil_types.fieldinfo -> 'a -> 'v) -> ('v, 'a) typ
val attribute : ('v, 's) typ -> string -> Cil_types.attrparam list -> ('v, 's) typ
val const : ('v, 's) typ -> ('v, 's) typ
val stdlib_generated : ('v, 's) typ -> ('v, 's) typ
val cil_typ : ('v, 's) typ -> Cil_types.typ
val cil_logic_type : ('v, 's) typ -> Cil_types.logic_type
type const' = Exp.const'
type var' = Exp.var'
type lval' = Exp.lval'
type exp' = Exp.exp'
type init' = Exp.init'
type label = Exp.label
type const = [
  1. | `const of const'
]
type var = [
  1. | `var of var'
]
type lval = [
  1. | var
  2. | `lval of lval'
]
type exp = [
  1. | const
  2. | lval
  3. | `exp of exp'
]
type init = [
  1. | exp
  2. | `init of init'
]
val pretty : Stdlib.Format.formatter -> [ init | `none ] -> unit
val none : [> `none ]
val here : label
val old : label
val pre : label
val post : label
val loop_entry : label
val loop_current : label
val program_init : label
val of_constant : Cil_types.constant -> [> const ]
val of_int : int -> [> const ]
val of_integer : Integer.t -> [> const ]
val zero : [> const ]
val one : [> const ]
val var : Cil_types.varinfo -> [> var ]
val of_lval : Cil_types.lval -> [> lval ]
exception EmptyList
val of_exp : Cil_types.exp -> [> exp ]
val of_exp_copy : Cil_types.exp -> [> exp ]
val of_exp_list : Cil_types.exp list -> [> exp ] list
val unop : Cil_types.unop -> [< exp ] -> [> exp ]
val neg : [< exp ] -> [> exp ]
val lognot : [< exp ] -> [> exp ]
val bwnot : [< exp ] -> [> exp ]
val succ : [< exp ] -> [> exp ]
val add_int : [< exp ] -> int -> [> exp ]
val binop : Cil_types.binop -> [< exp ] -> [< exp ] -> [> exp ]
val add : [< exp ] -> [< exp ] -> [> exp ]
val sub : [< exp ] -> [< exp ] -> [> exp ]
val mul : [< exp ] -> [< exp ] -> [> exp ]
val div : [< exp ] -> [< exp ] -> [> exp ]
val modulo : [< exp ] -> [< exp ] -> [> exp ]
val shiftl : [< exp ] -> [< exp ] -> [> exp ]
val shiftr : [< exp ] -> [< exp ] -> [> exp ]
val lt : [< exp ] -> [< exp ] -> [> exp ]
val gt : [< exp ] -> [< exp ] -> [> exp ]
val le : [< exp ] -> [< exp ] -> [> exp ]
val ge : [< exp ] -> [< exp ] -> [> exp ]
val eq : [< exp ] -> [< exp ] -> [> exp ]
val ne : [< exp ] -> [< exp ] -> [> exp ]
val logor : [< exp ] -> [< exp ] -> [> exp ]
val logand : [< exp ] -> [< exp ] -> [> exp ]
val logor_list : [< exp ] list -> exp
val logand_list : [< exp ] list -> exp
val bwand : [< exp ] -> [< exp ] -> [> exp ]
val bwor : [< exp ] -> [< exp ] -> [> exp ]
val bwxor : [< exp ] -> [< exp ] -> [> exp ]
val cast : ('v, 's) typ -> [< exp ] -> [> exp ]
val cast' : Cil_types.typ -> [< exp ] -> [> exp ]
val addr : [< lval ] -> [> exp ]
val mem : [< exp ] -> [> lval ]
val index : [< lval ] -> [< exp ] -> [> lval ]
val field : [< lval ] -> Cil_types.fieldinfo -> [> lval ]
val fieldnamed : [< lval ] -> string -> [> lval ]
val result : [> lval ]
val term : Cil_types.term -> [> exp ]
val range : [< exp | `none ] -> [< exp | `none ] -> [> exp ]
val whole : [> exp ]
val whole_right : [> exp ]
val app : Cil_types.logic_info -> label list -> [< exp ] list -> [> exp ]
val object_pointer : ?at:label -> [< exp ] -> [> exp ]
val valid : ?at:label -> [< exp ] -> [> exp ]
val valid_read : ?at:label -> [< exp ] -> [> exp ]
val initialized : ?at:label -> [< exp ] -> [> exp ]
val dangling : ?at:label -> [< exp ] -> [> exp ]
val allocable : ?at:label -> [< exp ] -> [> exp ]
val freeable : ?at:label -> [< exp ] -> [> exp ]
val fresh : label -> label -> [< exp ] -> [< exp ] -> [> exp ]
val of_init : Cil_types.init -> [> init ]
val compound : Cil_types.typ -> init list -> [> init ]
val values : (init, 'values) typ -> 'values -> init
val (+) : [< exp ] -> [< exp ] -> [> exp ]
val (-) : [< exp ] -> [< exp ] -> [> exp ]
val (*) : [< exp ] -> [< exp ] -> [> exp ]
val (/) : [< exp ] -> [< exp ] -> [> exp ]
val (%) : [< exp ] -> [< exp ] -> [> exp ]
val (<<) : [< exp ] -> [< exp ] -> [> exp ]
val (>>) : [< exp ] -> [< exp ] -> [> exp ]
val (<) : [< exp ] -> [< exp ] -> [> exp ]
val (>) : [< exp ] -> [< exp ] -> [> exp ]
val (<=) : [< exp ] -> [< exp ] -> [> exp ]
val (>=) : [< exp ] -> [< exp ] -> [> exp ]
val (==) : [< exp ] -> [< exp ] -> [> exp ]
val (!=) : [< exp ] -> [< exp ] -> [> exp ]
val (--) : [< exp ] -> [< exp ] -> [> exp ]
val (.@[]) : [< lval ] -> [< exp ] -> [> exp ]
exception LogicInC of exp
exception CInLogic of exp
exception NotATerm of exp
exception NotAPredicate of exp
exception NotAFunction of Cil_types.logic_info
exception Typing_error of string
exception OutOfScope of string
val cil_logic_label : label -> Cil_types.logic_label
val cil_constant : [< const ] -> Cil_types.constant
val cil_varinfo : [< var ] -> Cil_types.varinfo
val cil_lval : loc:Cil_types.location -> [< lval ] -> Cil_types.lval
val cil_exp : loc:Cil_types.location -> [< exp ] -> Cil_types.exp
val cil_term_lval : loc:Cil_types.location -> ?restyp:Cil_types.typ -> [< lval ] -> Cil_types.term_lval
val cil_term : loc:Cil_types.location -> ?restyp:Cil_types.typ -> [< exp ] -> Cil_types.term
val cil_iterm : loc:Cil_types.location -> ?restyp:Cil_types.typ -> [< exp ] -> Cil_types.identified_term
val cil_pred : loc:Cil_types.location -> ?restyp:Cil_types.typ -> [< exp ] -> Cil_types.predicate
val cil_ipred : loc:Cil_types.location -> ?restyp:Cil_types.typ -> [< exp ] -> Cil_types.identified_predicate
val cil_init : loc:Cil_types.location -> [< init ] -> Cil_types.init
val cil_typeof : [< var ] -> Cil_types.typ
val open_function : ?loc:Cil_types.location -> ?ghost:bool -> ?vorig_name:string -> string -> [> var ]
val set_return_type : ('s, 'v) typ -> unit
val set_return_type' : Cil_types.typ -> unit
val add_attribute : Cil_types.attribute -> unit
val add_new_attribute : string -> Cil_types.attrparam list -> unit
val add_stdlib_generated : unit -> unit
val finish_function : ?register:bool -> unit -> Cil_types.global
val finish_declaration : ?register:bool -> unit -> Cil_types.global
type source = [
  1. | exp
  2. | `indirect of exp
]
val indirect : [< source ] -> [> source ]
val assigns : [< exp ] list -> [< exp | `indirect of [< exp ] ] list -> unit
val requires : [< exp ] -> unit
val ensures : [< exp ] -> unit
val of_stmtkind : Cil_types.stmtkind -> unit
val of_stmt : Cil_types.stmt -> unit
val of_stmts : Cil_types.stmt list -> unit
val open_block : ?loc:Cil_types.location -> ?into:Cil_types.fundec -> ?ghost:bool -> unit -> unit
val open_ghost : ?loc:Cil_types.location -> ?into:Cil_types.fundec -> unit -> unit
val open_switch : ?loc:Cil_types.location -> ?into:Cil_types.fundec -> [< exp ] -> unit
val open_if : ?loc:Cil_types.location -> ?into:Cil_types.fundec -> [< exp ] -> unit
val open_else : ?ghost:bool -> unit -> unit
val close : unit -> unit
val finish_block : unit -> Cil_types.block
val finish_instr_list : ?scope:Cil_types.block -> unit -> Cil_types.instr list
val finish_stmt : unit -> Cil_types.stmt
val case : [< exp ] -> unit
val break : unit -> unit
val return : [< exp | `none ] -> unit
val local : ?ghost:bool -> ?init:'v -> (init, 'v) typ -> string -> [> var ]
val local' : ?ghost:bool -> ?init:init -> Cil_types.typ -> string -> [> var ]
val local_copy : ?ghost:bool -> ?suffix:string -> [< var ] -> [> var ]
val parameter : ?ghost:bool -> ?attributes:Cil_types.attributes -> Cil_types.typ -> string -> [> var ]
val of_instr : Cil_types.instr -> unit
val skip : unit -> unit
val assign : [< lval ] -> [< exp ] -> unit
val incr : [< lval ] -> unit
val call : [< lval | `none ] -> [< exp ] -> [< exp ] list -> unit
val pure : [< exp ] -> unit
val (:=) : [< lval ] -> [< exp ] -> unit
val (+=) : [< lval ] -> [< exp ] -> unit
val (-=) : [< lval ] -> [< exp ] -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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