Module Frama_c_kernel.Cabs

Untyped AST.

type cabsloc = Filepos.t * Filepos.t
val pp_cabsloc : Ppx_deriving_runtime.Format.formatter -> cabsloc -> Ppx_deriving_runtime.unit
val show_cabsloc : cabsloc -> Ppx_deriving_runtime.string
type typeSpecifier =
  1. | Tvoid
  2. | Tchar
  3. | Tbool
  4. | Tshort
  5. | Tint
  6. | Tlong
  7. | Tint64
  8. | Tint128
  9. | Tfloat
  10. | Tfloat32
  11. | Tfloat64
  12. | Tdouble
  13. | Tsigned
  14. | Tunsigned
  15. | Tnamed of string
  16. | Tstruct of string * field_group list option * attribute list
  17. | Tunion of string * field_group list option * attribute list
  18. | Tenum of string * enum_item list option * attribute list
  19. | TtypeofE of expression
  20. | 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_GHOST
and spec_elem =
  1. | SpecTypedef
  2. | SpecCV of cvspec
  3. | SpecAttr of attribute
  4. | SpecStorage of storage
  5. | SpecInline
  6. | SpecType of typeSpecifier
  7. | SpecAlignas of expression
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 = 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. | IF of expression * statement * statement * cabsloc
  5. | WHILE of loop_invariant * expression * statement * cabsloc
  6. | DOWHILE of loop_invariant * expression * statement * cabsloc
  7. | FOR of loop_invariant * for_clause * expression * expression * statement * cabsloc
  8. | BREAK of cabsloc
  9. | CONTINUE of cabsloc
  10. | RETURN of expression * cabsloc
  11. | SWITCH of expression * statement * cabsloc
  12. | CASE of expression * statement * cabsloc
  13. | CASERANGE of expression * expression * statement * cabsloc
  14. | DEFAULT of statement * cabsloc
  15. | LABEL of string * statement * cabsloc
  16. | GOTO of string * cabsloc
  17. | COMPGOTO of expression * cabsloc
  18. | DEFINITION of definition
  19. | ASM of attribute list * string list * asm_details option * cabsloc
  20. | 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.

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

    *)
  22. | CODE_ANNOT of Logic_ptree.code_annot * cabsloc
  23. | 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 * [ `Standard | `GCC ]
  15. | TYPE_ALIGNOF of specifier * decl_type * [ `Standard | `GCC ]
  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_BOOL of bool
  2. | CONST_INT of string
  3. | CONST_FLOAT of string
  4. | CONST_CHAR of int64 list
  5. | CONST_WCHAR of int64 list
  6. | CONST_STRING of string
  7. | 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
val pp_typeSpecifier : Ppx_deriving_runtime.Format.formatter -> typeSpecifier -> Ppx_deriving_runtime.unit
val show_typeSpecifier : typeSpecifier -> Ppx_deriving_runtime.string
val pp_storage : Ppx_deriving_runtime.Format.formatter -> storage -> Ppx_deriving_runtime.unit
val show_storage : storage -> Ppx_deriving_runtime.string
val pp_cvspec : Ppx_deriving_runtime.Format.formatter -> cvspec -> Ppx_deriving_runtime.unit
val show_cvspec : cvspec -> Ppx_deriving_runtime.string
val pp_spec_elem : Ppx_deriving_runtime.Format.formatter -> spec_elem -> Ppx_deriving_runtime.unit
val show_spec_elem : spec_elem -> Ppx_deriving_runtime.string
val pp_specifier : Ppx_deriving_runtime.Format.formatter -> specifier -> Ppx_deriving_runtime.unit
val show_specifier : specifier -> Ppx_deriving_runtime.string
val pp_decl_type : Ppx_deriving_runtime.Format.formatter -> decl_type -> Ppx_deriving_runtime.unit
val show_decl_type : decl_type -> Ppx_deriving_runtime.string
val pp_name_group : Ppx_deriving_runtime.Format.formatter -> name_group -> Ppx_deriving_runtime.unit
val show_name_group : name_group -> Ppx_deriving_runtime.string
val pp_field_group : Ppx_deriving_runtime.Format.formatter -> field_group -> Ppx_deriving_runtime.unit
val show_field_group : field_group -> Ppx_deriving_runtime.string
val pp_init_name_group : Ppx_deriving_runtime.Format.formatter -> init_name_group -> Ppx_deriving_runtime.unit
val show_init_name_group : init_name_group -> Ppx_deriving_runtime.string
val pp_name : Ppx_deriving_runtime.Format.formatter -> name -> Ppx_deriving_runtime.unit
val show_name : name -> Ppx_deriving_runtime.string
val pp_init_name : Ppx_deriving_runtime.Format.formatter -> init_name -> Ppx_deriving_runtime.unit
val show_init_name : init_name -> Ppx_deriving_runtime.string
val pp_single_name : Ppx_deriving_runtime.Format.formatter -> single_name -> Ppx_deriving_runtime.unit
val show_single_name : single_name -> Ppx_deriving_runtime.string
val pp_enum_item : Ppx_deriving_runtime.Format.formatter -> enum_item -> Ppx_deriving_runtime.unit
val show_enum_item : enum_item -> Ppx_deriving_runtime.string
val pp_definition : Ppx_deriving_runtime.Format.formatter -> definition -> Ppx_deriving_runtime.unit
val show_definition : definition -> Ppx_deriving_runtime.string
val pp_file : Ppx_deriving_runtime.Format.formatter -> file -> Ppx_deriving_runtime.unit
val show_file : file -> Ppx_deriving_runtime.string
val pp_block : Ppx_deriving_runtime.Format.formatter -> block -> Ppx_deriving_runtime.unit
val show_block : block -> Ppx_deriving_runtime.string
val pp_asm_details : Ppx_deriving_runtime.Format.formatter -> asm_details -> Ppx_deriving_runtime.unit
val show_asm_details : asm_details -> Ppx_deriving_runtime.string
val pp_raw_statement : Ppx_deriving_runtime.Format.formatter -> raw_statement -> Ppx_deriving_runtime.unit
val show_raw_statement : raw_statement -> Ppx_deriving_runtime.string
val pp_statement : Ppx_deriving_runtime.Format.formatter -> statement -> Ppx_deriving_runtime.unit
val show_statement : statement -> Ppx_deriving_runtime.string
val pp_loop_invariant : Ppx_deriving_runtime.Format.formatter -> loop_invariant -> Ppx_deriving_runtime.unit
val show_loop_invariant : loop_invariant -> Ppx_deriving_runtime.string
val pp_for_clause : Ppx_deriving_runtime.Format.formatter -> for_clause -> Ppx_deriving_runtime.unit
val show_for_clause : for_clause -> Ppx_deriving_runtime.string
val pp_binary_operator : Ppx_deriving_runtime.Format.formatter -> binary_operator -> Ppx_deriving_runtime.unit
val show_binary_operator : binary_operator -> Ppx_deriving_runtime.string
val pp_unary_operator : Ppx_deriving_runtime.Format.formatter -> unary_operator -> Ppx_deriving_runtime.unit
val show_unary_operator : unary_operator -> Ppx_deriving_runtime.string
val pp_expression : Ppx_deriving_runtime.Format.formatter -> expression -> Ppx_deriving_runtime.unit
val show_expression : expression -> Ppx_deriving_runtime.string
val pp_cabsexp : Ppx_deriving_runtime.Format.formatter -> cabsexp -> Ppx_deriving_runtime.unit
val show_cabsexp : cabsexp -> Ppx_deriving_runtime.string
val pp_constant : Ppx_deriving_runtime.Format.formatter -> constant -> Ppx_deriving_runtime.unit
val show_constant : constant -> Ppx_deriving_runtime.string
val pp_init_expression : Ppx_deriving_runtime.Format.formatter -> init_expression -> Ppx_deriving_runtime.unit
val show_init_expression : init_expression -> Ppx_deriving_runtime.string
val pp_initwhat : Ppx_deriving_runtime.Format.formatter -> initwhat -> Ppx_deriving_runtime.unit
val show_initwhat : initwhat -> Ppx_deriving_runtime.string
val pp_attribute : Ppx_deriving_runtime.Format.formatter -> attribute -> Ppx_deriving_runtime.unit
val show_attribute : attribute -> Ppx_deriving_runtime.string