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.1-Nickel.tar.gz
sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

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

Module Frama_c_kernel.Cabs

Untyped AST.

type typeSpecifier =
  1. | Tvoid
  2. | Tchar
  3. | Tbool
  4. | Tshort
  5. | Tint
  6. | Tlong
  7. | Tint64
  8. | Tfloat
  9. | Tdouble
  10. | Tsigned
  11. | Tunsigned
  12. | Tnamed of string
  13. | Tstruct of string * field_group list option * attribute list
  14. | Tunion of string * field_group list option * attribute list
  15. | Tenum of string * enum_item list option * attribute list
  16. | TtypeofE of expression
  17. | TtypeofT of specifier * decl_type
and storage =
  1. | NO_STORAGE
  2. | AUTO
  3. | STATIC
  4. | EXTERN
  5. | REGISTER
and funspec =
  1. | INLINE
  2. | VIRTUAL
  3. | EXPLICIT
and cvspec =
  1. | CV_CONST
  2. | CV_VOLATILE
  3. | CV_RESTRICT
  4. | CV_ATTRIBUTE_ANNOT of string
  5. | CV_GHOST
and spec_elem =
  1. | SpecTypedef
  2. | SpecCV of cvspec
  3. | SpecAttr of attribute
  4. | SpecStorage of storage
  5. | SpecInline
  6. | SpecType of typeSpecifier
  7. | SpecPattern of string
and specifier = spec_elem list
and decl_type =
  1. | JUSTBASE
  2. | PARENTYPE of attribute list * decl_type * attribute list
  3. | ARRAY of decl_type * attribute list * expression
  4. | PTR of attribute list * decl_type
  5. | PROTO of decl_type * single_name list * single_name list * bool
and name_group = specifier * name list
and field_group =
  1. | FIELD of specifier * (name * expression option) list
  2. | TYPE_ANNOT of Logic_ptree.type_annot
  3. | STATIC_ASSERT_FG of expression * string * cabsloc
and init_name_group = specifier * init_name list
and name = string * decl_type * attribute list * cabsloc
and init_name = name * init_expression
and single_name = specifier * name
and enum_item = string * expression * cabsloc
and definition =
  1. | FUNDEF of (Logic_ptree.spec * cabsloc) option * single_name * block * cabsloc * cabsloc
  2. | DECDEF of (Logic_ptree.spec * cabsloc) option * init_name_group * cabsloc
  3. | TYPEDEF of name_group * cabsloc
  4. | ONLYTYPEDEF of specifier * cabsloc
  5. | GLOBASM of string * cabsloc
  6. | PRAGMA of expression * cabsloc
  7. | STATIC_ASSERT of expression * string * cabsloc
  8. | LINKAGE of string * cabsloc * definition list
  9. | GLOBANNOT of Logic_ptree.decl list
and file = Datatype.Filepath.t * (bool * definition) list

the file name, and then the list of toplevel forms.

and block = {
  1. blabels : string list;
  2. battrs : attribute list;
  3. bstmts : statement list;
}
and asm_details = {
  1. aoutputs : (string option * string * expression) list;
  2. ainputs : (string option * string * expression) list;
  3. aclobbers : string list;
  4. alabels : string list;
}
and raw_statement =
  1. | NOP of cabsloc
  2. | COMPUTATION of expression * cabsloc
  3. | BLOCK of block * cabsloc * cabsloc
  4. | SEQUENCE of statement * statement * cabsloc
  5. | IF of expression * statement * statement * cabsloc
  6. | WHILE of loop_invariant * expression * statement * cabsloc
  7. | DOWHILE of loop_invariant * expression * statement * cabsloc
  8. | FOR of loop_invariant * for_clause * expression * expression * statement * cabsloc
  9. | BREAK of cabsloc
  10. | CONTINUE of cabsloc
  11. | RETURN of expression * cabsloc
  12. | SWITCH of expression * statement * cabsloc
  13. | CASE of expression * statement * cabsloc
  14. | CASERANGE of expression * expression * statement * cabsloc
  15. | DEFAULT of statement * cabsloc
  16. | LABEL of string * statement * cabsloc
  17. | GOTO of string * cabsloc
  18. | COMPGOTO of expression * cabsloc
  19. | DEFINITION of definition
  20. | ASM of attribute list * string list * asm_details option * cabsloc
  21. | THROW of expression option * cabsloc
    (*

    throws the corresponding expression. None corresponds to re-throwing the exception currently being caught (thus is only meaningful in a catch clause). This node is not generated by the C parser, but can be used by external front-ends.

    *)
  22. | TRY_CATCH of statement * (single_name option * statement) list * cabsloc
    (*

    TRY_CATCH(s,clauses,loc) catches exceptions thrown by execution of s, according to clauses. An exception e is caught by the first clause (spec,(name, decl, _, _)),body such that the type of e is compatible with (spec,decl). name is then associated to a copy of e, and body is executed. If the single_name is None, all exceptions are caught by the corresponding clause.

    The corresponding TryCatch node in Cil_types.stmtkind has a refined notion of catching that allows a clause to match for more than one type using appropriate conversions (see also Cil_types.catch_binder).

    This node is not generated by the C parser, but can be used by external front-ends.

    *)
  23. | TRY_EXCEPT of block * expression * block * cabsloc
    (*

    MS SEH

    *)
  24. | TRY_FINALLY of block * block * cabsloc
    (*

    MS SEH

    *)
  25. | CODE_ANNOT of Logic_ptree.code_annot * cabsloc
  26. | CODE_SPEC of Logic_ptree.spec * cabsloc
and statement = {
  1. mutable stmt_ghost : bool;
  2. stmt_node : raw_statement;
}
and loop_invariant = Logic_ptree.code_annot list
and for_clause =
  1. | FC_EXP of expression
  2. | FC_DECL of definition
and binary_operator =
  1. | ADD
  2. | SUB
  3. | MUL
  4. | DIV
  5. | MOD
  6. | AND
  7. | OR
  8. | BAND
  9. | BOR
  10. | XOR
  11. | SHL
  12. | SHR
  13. | EQ
  14. | NE
  15. | LT
  16. | GT
  17. | LE
  18. | GE
  19. | ASSIGN
  20. | ADD_ASSIGN
  21. | SUB_ASSIGN
  22. | MUL_ASSIGN
  23. | DIV_ASSIGN
  24. | MOD_ASSIGN
  25. | BAND_ASSIGN
  26. | BOR_ASSIGN
  27. | XOR_ASSIGN
  28. | SHL_ASSIGN
  29. | SHR_ASSIGN
and unary_operator =
  1. | MINUS
  2. | PLUS
  3. | NOT
  4. | BNOT
  5. | MEMOF
  6. | ADDROF
  7. | PREINCR
  8. | PREDECR
  9. | POSINCR
  10. | POSDECR
and expression = {
  1. expr_loc : cabsloc;
  2. expr_node : cabsexp;
}
and cabsexp =
  1. | NOTHING
  2. | UNARY of unary_operator * expression
  3. | LABELADDR of string
  4. | BINARY of binary_operator * expression * expression
  5. | QUESTION of expression * expression * expression
  6. | CAST of specifier * decl_type * init_expression
  7. | CALL of expression * expression list * expression list
  8. | COMMA of expression list
  9. | CONSTANT of constant
  10. | PAREN of expression
  11. | VARIABLE of string
  12. | EXPR_SIZEOF of expression
  13. | TYPE_SIZEOF of specifier * decl_type
  14. | EXPR_ALIGNOF of expression
  15. | TYPE_ALIGNOF of specifier * decl_type
  16. | INDEX of expression * expression
  17. | MEMBEROF of expression * string
  18. | MEMBEROFPTR of expression * string
  19. | GNU_BODY of block
  20. | EXPR_PATTERN of string
  21. | GENERIC of expression * ((specifier * decl_type) option * expression) list
and constant =
  1. | CONST_INT of string
  2. | CONST_FLOAT of string
  3. | CONST_CHAR of int64 list
  4. | CONST_WCHAR of int64 list
  5. | CONST_STRING of string
  6. | CONST_WSTRING of int64 list
and init_expression =
  1. | NO_INIT
  2. | SINGLE_INIT of expression
  3. | COMPOUND_INIT of (initwhat * init_expression) list
and initwhat =
  1. | NEXT_INIT
  2. | INFIELD_INIT of string * initwhat
  3. | ATINDEX_INIT of expression * initwhat
  4. | ATINDEXRANGE_INIT of expression * expression
and attribute = string * expression list