package frama-c

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

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 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
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. | 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. | CODE_ANNOT of Logic_ptree.code_annot * cabsloc
  24. | 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. | 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
OCaml

Innovation. Community. Security.

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