Module Frama_c_kernel.Cabs

Untyped AST.

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 storage =
| NO_STORAGE
| AUTO
| STATIC
| EXTERN
| REGISTER
and funspec =
| INLINE
| VIRTUAL
| EXPLICIT
and cvspec =
| CV_CONST
| CV_VOLATILE
| CV_RESTRICT
| CV_ATTRIBUTE_ANNOT of string
| CV_GHOST
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 name_group = specifier * name list
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_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 =
| 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 block = {
blabels : string list;
battrs : attribute list;
bstmts : statement list;
}
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. 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.

*)
| 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.

*)
| 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 statement = {
mutable stmt_ghost : bool;
stmt_node : raw_statement;
}
and loop_invariant = Logic_ptree.code_annot list
and for_clause =
| FC_EXP of expression
| FC_DECL of definition
and binary_operator =
| ADD
| SUB
| MUL
| DIV
| MOD
| AND
| OR
| BAND
| BOR
| XOR
| SHL
| SHR
| EQ
| NE
| LT
| GT
| LE
| GE
| ASSIGN
| ADD_ASSIGN
| SUB_ASSIGN
| MUL_ASSIGN
| DIV_ASSIGN
| MOD_ASSIGN
| BAND_ASSIGN
| BOR_ASSIGN
| XOR_ASSIGN
| SHL_ASSIGN
| SHR_ASSIGN
and unary_operator =
| MINUS
| PLUS
| NOT
| BNOT
| MEMOF
| ADDROF
| PREINCR
| PREDECR
| POSINCR
| POSDECR
and expression = {
expr_loc : cabsloc;
expr_node : cabsexp;
}
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 constant =
| CONST_INT of string
| CONST_FLOAT of string
| CONST_CHAR of int64 list
| CONST_WCHAR of int64 list
| CONST_STRING of string
| CONST_WSTRING of int64 list
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