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 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 attribute option * 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