package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. P
    Pierre Nigron
  36. A
    Anne Pacalet
  37. V
    Valentin Perrelle
  38. G
    Guillaume Petiot
  39. D
    Dario Pinto
  40. V
    Virgile Prevosto
  41. A
    Armand Puccetti
  42. F
    Félix Ridoux
  43. V
    Virgile Robles
  44. J
    Jan Rochel
  45. M
    Muriel Roger
  46. J
    Julien Signoles
  47. N
    Nicolas Stouls
  48. K
    Kostyantyn Vorobyov
  49. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-28.0-Nickel.tar.gz
sha256=29612882330ecb6eddd0b4ca3afc0492b70d0feb3379a1b8e893194c6e173983

doc/frama-c.kernel/Frama_c_kernel/Cil_builder/Pure/index.html

Module Cil_builder.Pure

include module type of Exp
include module type of Type
exception NotACType
type ('value, 'shape) 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 uint : ('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'
type var'
type lval'
type exp'
type init'
type 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 : 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_int : int -> [> const ]

Implicitly converted to type int when converted into C constant

val of_integer : Integer.t -> [> const ]

Implicitly converted to type int when converted into C constant

val of_cint : ?kind:Cil_types.ikind -> Integer.t -> [> const ]

Default kind is int. Value is truncated if necessary.

val of_cfloat : ?kind:Cil_types.fkind -> float -> [> const ]

Default kind is double. Value is rounded to simple precision if necessary.

val of_constant : Cil_types.constant -> [> 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
type instr'
type stmt'
type instr = [
  1. | `instr of instr'
]
type stmt = [
  1. | instr
  2. | `stmt of stmt'
]
val of_instr : Cil_types.instr -> [> instr ]
val skip : [> instr ]
val assign : [< lval ] -> [< exp ] -> [> instr ]
val incr : [< lval ] -> [> instr ]
val call : [< lval | `none ] -> [< exp ] -> [< exp ] list -> [> instr ]
val local : ?ghost:bool -> ?init:'v -> (init, 'v) typ -> string -> [> var ] * [> instr ]
val local' : ?ghost:bool -> ?init:init -> Cil_types.typ -> string -> [> var ] * [> instr ]
val local_copy : ?ghost:bool -> ?suffix:string -> [< var ] -> [> var ] * [> instr ]
val of_stmtkind : Cil_types.stmtkind -> [> stmt ]
val of_stmt : Cil_types.stmt -> [> stmt ]
val of_stmts : Cil_types.stmt list -> [> stmt ]
val block : [< stmt ] list -> [> stmt ]
val sequence : [< stmt ] list -> [> stmt ]
val ghost : [< stmt ] -> [> stmt ]
val if_ : ?ghost_else:bool -> [< exp ] -> then_:[< stmt ] list -> else_:[< stmt ] list -> [> stmt ]
val cil_instr : ?into:Cil_types.fundec -> loc:Cil_types.location -> instr -> Cil_types.instr
val cil_stmtkind : ?into:Cil_types.fundec -> loc:Cil_types.location -> stmt -> Cil_types.stmtkind
val cil_stmt : ?into:Cil_types.fundec -> loc:Cil_types.location -> stmt -> Cil_types.stmt
val (let+) : (var * stmt) -> (var -> stmt list) -> stmt list
val (and+) : var -> var -> var * var
val (:=) : [< lval ] -> [< exp ] -> [> instr ]
val (+=) : [< lval ] -> [< exp ] -> [> instr ]
val (-=) : [< lval ] -> [< exp ] -> [> instr ]