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
  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