Frama_c_kernel.Cabs
Untyped AST.
type cabsloc = Filepath.position * Filepath.position
type typeSpecifier =
| Tvoid |
| Tchar |
| Tbool |
| Tshort |
| Tint |
| Tlong |
| Tint64 |
| Tfloat |
| Tdouble |
| Tsigned |
| Tunsigned |
| Tnamed of string |
| Tstruct of string * field_group list option * attribute list |
| Tunion of string * field_group list option * attribute list |
| Tenum of string * enum_item list option * attribute list |
| TtypeofE of expression |
| TtypeofT of specifier * decl_type |
and spec_elem =
| SpecTypedef |
| SpecCV of cvspec |
| SpecAttr of attribute |
| SpecStorage of storage |
| SpecInline |
| SpecType of typeSpecifier |
| SpecPattern of string |
and specifier = spec_elem list
and decl_type =
| JUSTBASE |
| PARENTYPE of attribute list * decl_type * attribute list |
| ARRAY of decl_type * attribute list * expression |
| PTR of attribute list * decl_type |
| PROTO of decl_type * single_name list * single_name list * bool |
and field_group =
| FIELD of specifier * (name * expression option) list |
| TYPE_ANNOT of Logic_ptree.type_annot |
| STATIC_ASSERT_FG of expression * string * cabsloc |
and init_name = name * init_expression
and enum_item = string * expression * cabsloc
and definition =
| FUNDEF of (Logic_ptree.spec * cabsloc) option
* single_name
* block
* cabsloc
* cabsloc |
| DECDEF of (Logic_ptree.spec * cabsloc) option * init_name_group * cabsloc |
| TYPEDEF of name_group * cabsloc |
| ONLYTYPEDEF of specifier * cabsloc |
| GLOBASM of string * cabsloc |
| PRAGMA of expression * cabsloc |
| STATIC_ASSERT of expression * string * cabsloc |
| LINKAGE of string * cabsloc * definition list |
| 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 asm_details = {
aoutputs : (string option * string * expression) list; |
ainputs : (string option * string * expression) list; |
aclobbers : string list; |
alabels : string list; |
}
and raw_statement =
| NOP of cabsloc | |
| COMPUTATION of expression * cabsloc | |
| BLOCK of block * cabsloc * cabsloc | |
| SEQUENCE of statement * statement * cabsloc | |
| IF of expression * statement * statement * cabsloc | |
| WHILE of loop_invariant * expression * statement * cabsloc | |
| DOWHILE of loop_invariant * expression * statement * cabsloc | |
| FOR of loop_invariant
* for_clause
* expression
* expression
* statement
* cabsloc | |
| BREAK of cabsloc | |
| CONTINUE of cabsloc | |
| RETURN of expression * cabsloc | |
| SWITCH of expression * statement * cabsloc | |
| CASE of expression * statement * cabsloc | |
| CASERANGE of expression * expression * statement * cabsloc | |
| DEFAULT of statement * cabsloc | |
| LABEL of string * statement * cabsloc | |
| GOTO of string * cabsloc | |
| COMPGOTO of expression * cabsloc | |
| DEFINITION of definition | |
| ASM of attribute list * string list * asm_details option * cabsloc | |
| THROW of expression option * cabsloc | (* throws the corresponding expression. |
| TRY_CATCH of statement * (single_name option * statement) list * cabsloc | (*
The corresponding This node is not generated by the C parser, but can be used by external front-ends. *) |
| TRY_EXCEPT of block * expression * block * cabsloc | (* MS SEH *) |
| TRY_FINALLY of block * block * cabsloc | (* MS SEH *) |
| CODE_ANNOT of Logic_ptree.code_annot * cabsloc | |
| CODE_SPEC of Logic_ptree.spec * cabsloc |
and loop_invariant = Logic_ptree.code_annot list
and cabsexp =
| NOTHING |
| UNARY of unary_operator * expression |
| LABELADDR of string |
| BINARY of binary_operator * expression * expression |
| QUESTION of expression * expression * expression |
| CAST of specifier * decl_type * init_expression |
| CALL of expression * expression list * expression list |
| COMMA of expression list |
| CONSTANT of constant |
| PAREN of expression |
| VARIABLE of string |
| EXPR_SIZEOF of expression |
| TYPE_SIZEOF of specifier * decl_type |
| EXPR_ALIGNOF of expression |
| TYPE_ALIGNOF of specifier * decl_type |
| INDEX of expression * expression |
| MEMBEROF of expression * string |
| MEMBEROFPTR of expression * string |
| GNU_BODY of block |
| EXPR_PATTERN of string |
and init_expression =
| NO_INIT |
| SINGLE_INIT of expression |
| COMPOUND_INIT of (initwhat * init_expression) list |
and initwhat =
| NEXT_INIT |
| INFIELD_INIT of string * initwhat |
| ATINDEX_INIT of expression * initwhat |
| ATINDEXRANGE_INIT of expression * expression |
and attribute = string * expression list