sig
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 * Cabs.field_group list option * Cabs.attribute list
| Tunion of string * Cabs.field_group list option * Cabs.attribute list
| Tenum of string * Cabs.enum_item list option * Cabs.attribute list
| TtypeofE of Cabs.expression
| TtypeofT of Cabs.specifier * Cabs.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 Cabs.cvspec
| SpecAttr of Cabs.attribute
| SpecStorage of Cabs.storage
| SpecInline
| SpecType of Cabs.typeSpecifier
| SpecPattern of string
and specifier = Cabs.spec_elem list
and decl_type =
JUSTBASE
| PARENTYPE of Cabs.attribute list * Cabs.decl_type * Cabs.attribute list
| ARRAY of Cabs.decl_type * Cabs.attribute list * Cabs.expression
| PTR of Cabs.attribute list * Cabs.decl_type
| PROTO of Cabs.decl_type * Cabs.single_name list *
Cabs.single_name list * bool
and name_group = Cabs.specifier * Cabs.name list
and field_group =
FIELD of Cabs.specifier * (Cabs.name * Cabs.expression option) list
| TYPE_ANNOT of Logic_ptree.type_annot
| STATIC_ASSERT_FG of Cabs.expression * string * Cabs.cabsloc
and init_name_group = Cabs.specifier * Cabs.init_name list
and name = string * Cabs.decl_type * Cabs.attribute list * Cabs.cabsloc
and init_name = Cabs.name * Cabs.init_expression
and single_name = Cabs.specifier * Cabs.name
and enum_item = string * Cabs.expression * Cabs.cabsloc
and definition =
FUNDEF of (Logic_ptree.spec * Cabs.cabsloc) option * Cabs.single_name *
Cabs.block * Cabs.cabsloc * Cabs.cabsloc
| DECDEF of (Logic_ptree.spec * Cabs.cabsloc) option *
Cabs.init_name_group * Cabs.cabsloc
| TYPEDEF of Cabs.name_group * Cabs.cabsloc
| ONLYTYPEDEF of Cabs.specifier * Cabs.cabsloc
| GLOBASM of string * Cabs.cabsloc
| PRAGMA of Cabs.expression * Cabs.cabsloc
| STATIC_ASSERT of Cabs.expression * string * Cabs.cabsloc
| LINKAGE of string * Cabs.cabsloc * Cabs.definition list
| GLOBANNOT of Logic_ptree.decl list
| CUSTOM of Logic_ptree.custom_tree * string * Cabs.cabsloc
and file = Datatype.Filepath.t * (bool * Cabs.definition) list
and block = {
blabels : string list;
battrs : Cabs.attribute list;
bstmts : Cabs.statement list;
}
and asm_details = {
aoutputs : (string option * string * Cabs.expression) list;
ainputs : (string option * string * Cabs.expression) list;
aclobbers : string list;
alabels : string list;
}
and raw_statement =
NOP of Cabs.cabsloc
| COMPUTATION of Cabs.expression * Cabs.cabsloc
| BLOCK of Cabs.block * Cabs.cabsloc * Cabs.cabsloc
| SEQUENCE of Cabs.statement * Cabs.statement * Cabs.cabsloc
| IF of Cabs.expression * Cabs.statement * Cabs.statement * Cabs.cabsloc
| WHILE of Cabs.loop_invariant * Cabs.expression * Cabs.statement *
Cabs.cabsloc
| DOWHILE of Cabs.loop_invariant * Cabs.expression * Cabs.statement *
Cabs.cabsloc
| FOR of Cabs.loop_invariant * Cabs.for_clause * Cabs.expression *
Cabs.expression * Cabs.statement * Cabs.cabsloc
| BREAK of Cabs.cabsloc
| CONTINUE of Cabs.cabsloc
| RETURN of Cabs.expression * Cabs.cabsloc
| SWITCH of Cabs.expression * Cabs.statement * Cabs.cabsloc
| CASE of Cabs.expression * Cabs.statement * Cabs.cabsloc
| CASERANGE of Cabs.expression * Cabs.expression * Cabs.statement *
Cabs.cabsloc
| DEFAULT of Cabs.statement * Cabs.cabsloc
| LABEL of string * Cabs.statement * Cabs.cabsloc
| GOTO of string * Cabs.cabsloc
| COMPGOTO of Cabs.expression * Cabs.cabsloc
| DEFINITION of Cabs.definition
| ASM of Cabs.attribute list * string list * Cabs.asm_details option *
Cabs.cabsloc
| THROW of Cabs.expression option * Cabs.cabsloc
| TRY_CATCH of Cabs.statement *
(Cabs.single_name option * Cabs.statement) list * Cabs.cabsloc
| TRY_EXCEPT of Cabs.block * Cabs.expression * Cabs.block * Cabs.cabsloc
| TRY_FINALLY of Cabs.block * Cabs.block * Cabs.cabsloc
| CODE_ANNOT of (Logic_ptree.code_annot * Cabs.cabsloc)
| CODE_SPEC of (Logic_ptree.spec * Cabs.cabsloc)
and statement = {
mutable stmt_ghost : bool;
stmt_node : Cabs.raw_statement;
}
and loop_invariant = Logic_ptree.code_annot list
and for_clause = FC_EXP of Cabs.expression | FC_DECL of Cabs.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 : Cabs.cabsloc; expr_node : Cabs.cabsexp; }
and cabsexp =
NOTHING
| UNARY of Cabs.unary_operator * Cabs.expression
| LABELADDR of string
| BINARY of Cabs.binary_operator * Cabs.expression * Cabs.expression
| QUESTION of Cabs.expression * Cabs.expression * Cabs.expression
| CAST of (Cabs.specifier * Cabs.decl_type) * Cabs.init_expression
| CALL of Cabs.expression * Cabs.expression list * Cabs.expression list
| COMMA of Cabs.expression list
| CONSTANT of Cabs.constant
| PAREN of Cabs.expression
| VARIABLE of string
| EXPR_SIZEOF of Cabs.expression
| TYPE_SIZEOF of Cabs.specifier * Cabs.decl_type
| EXPR_ALIGNOF of Cabs.expression
| TYPE_ALIGNOF of Cabs.specifier * Cabs.decl_type
| INDEX of Cabs.expression * Cabs.expression
| MEMBEROF of Cabs.expression * string
| MEMBEROFPTR of Cabs.expression * string
| GNU_BODY of Cabs.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 Cabs.expression
| COMPOUND_INIT of (Cabs.initwhat * Cabs.init_expression) list
and initwhat =
NEXT_INIT
| INFIELD_INIT of string * Cabs.initwhat
| ATINDEX_INIT of Cabs.expression * Cabs.initwhat
| ATINDEXRANGE_INIT of Cabs.expression * Cabs.expression
and attribute = string * Cabs.expression list
end