package frama-clang

  1. Overview
  2. Docs
type location = Stdlib.Lexing.position * Stdlib.Lexing.position
type ikind =
  1. | IBool
  2. | IChar_u
  3. | IChar_s
  4. | IUChar
  5. | ISChar
  6. | IChar16
  7. | IChar32
  8. | IWChar_u
  9. | IWChar_s
  10. | IChar
  11. | IWChar
  12. | IShort
  13. | IUShort
  14. | IInt
  15. | IUInt
  16. | ILong
  17. | IULong
  18. | ILongLong
  19. | IULongLong
and fkind =
  1. | FFloat
  2. | FDouble
  3. | FLongDouble
and ickind =
  1. | ICLiteral
  2. | ICStaticConst
  3. | ICExternConst
and tcckind =
  1. | TCCSizeOf
  2. | TCCAlignOf
and compilation_constant =
  1. | IntCst of ikind * ickind * Stdlib.Int64.t
  2. | FloatCst of fkind * string
  3. | EnumCst of qualified_name * ekind * Stdlib.Int64.t
  4. | TypeCst of tcckind * typ
and template_parameter =
  1. | TPStructOrClass of qualified_name
  2. | TPTypename of qual_type
  3. | TPConstant of compilation_constant
  4. | TPDeclaration of qualified_name
and qualification =
  1. | QNamespace of string
  2. | QStructOrClass of string
  3. | QTemplateInstance of string * template_parameter list
and qualified_name = {
  1. prequalification : qualification list;
  2. decl_name : string;
}
and ekind = {
  1. body : qualified_name;
  2. ekind_is_extern_c : bool;
}
and funkind =
  1. | FKFunction
  2. | FKMethod of specifier list
  3. | FKCastMethodOperator of specifier list * qual_type
  4. | FKConstructor of bool
  5. | FKDestructor of bool
and signature = {
  1. result : qual_type;
  2. parameter : qual_type list;
  3. variadic : bool;
}
and pkind =
  1. | PDataPointer of qual_type
  2. | PFunctionPointer of signature
  3. | PStandardMethodPointer of signature * Stdlib.Int64.t
  4. | PVirtualMethodPointer of signature * Stdlib.Int64.t * Stdlib.Int64.t
and akind = {
  1. subtype : qual_type;
  2. dimension : expression option;
}
and ckind =
  1. | CClass
  2. | CStruct
  3. | CUnion
and tkind =
  1. | TStandard
  2. | TTemplateInstance of template_parameter list
and vkind =
  1. | VStandard
  2. | VVirtual
and typ =
  1. | Void
  2. | Int of ikind
  3. | Enum of ekind
  4. | Float of fkind
  5. | Pointer of pkind
  6. | LVReference of pkind
  7. | RVReference of pkind
  8. | Array of akind
  9. | Struct of qualified_name * tkind
  10. | Union of qualified_name * tkind
  11. | Named of qualified_name * bool
  12. | Lambda of signature list * capture list
and specifier =
  1. | Const
  2. | Volatile
  3. | Restrict
  4. | Static
and qual_type = {
  1. qualifier : specifier list;
  2. plain_type : typ;
}
and arg_decl = {
  1. arg_type : qual_type;
  2. arg_name : string;
  3. arg_loc : location;
}
and expression = {
  1. eloc : location;
  2. econtent : exp_node;
}
and variable =
  1. | Local of qualified_name
  2. | Global of qualified_name
  3. | FunctionParameter of string
  4. | CodePointer of qualified_name * signature * funkind * bool * tkind
and uokind =
  1. | UOCastNoEffect of qual_type
  2. | UOCastDeref
  3. | UOCastDerefInit
  4. | UOCastToVoid
  5. | UOCastInteger of qual_type * ikind
  6. | UOCastEnum of qual_type * ekind
  7. | UOCastFloat of qual_type * fkind
  8. | UOCastC of qual_type
  9. | UOPostInc
  10. | UOPostDec
  11. | UOPreInc
  12. | UOPreDec
  13. | UOOpposite
  14. | UOBitNegate
  15. | UOLogicalNegate
and bokind =
  1. | BOPlus
  2. | BOMinus
  3. | BOLess
  4. | BOLessOrEqual
  5. | BOEqual
  6. | BODifferent
  7. | BOGreaterOrEqual
  8. | BOGreater
  9. | BOTimes
  10. | BODivide
  11. | BOModulo
  12. | BOBitOr
  13. | BOBitAnd
  14. | BOBitExclusiveOr
  15. | BOLeftShift
  16. | BORightShift
  17. | BOLogicalAnd
  18. | BOLogicalOr
  19. | BOComma
and assign_kind =
  1. | AKRValue
  2. | AKAssign
and reference_or_pointer_kind =
  1. | RPKPointer
  2. | RPKReference
  3. | RPKStaticBasePointer
  4. | RPKStaticBaseReference
  5. | RPKVirtualBasePointer of Stdlib.Int64.t * qual_type * bool
  6. | RPKVirtualBaseReference of Stdlib.Int64.t * qual_type
  7. | RPKDynamicPointer of qual_type * expression
  8. | RPKDynamicReference of qual_type * expression
and lambda_overload_instance = {
  1. return_type : qual_type;
  2. arg_decls : arg_decl list;
  3. id : Stdlib.Int64.t;
  4. impl : statement list;
}
and exp_node =
  1. | Constant of compilation_constant
  2. | String of string
  3. | Variable of variable
  4. | Malloc of typ
  5. | MallocArray of typ * expression
  6. | Free of expression
  7. | FreeArray of expression
  8. | Assign of expression * expression
  9. | Unary_operator of uokind * expression
  10. | Binary_operator of bokind * assign_kind * expression * expression
  11. | Dereference of expression
  12. | Address of expression
  13. | PointerCast of qual_type * reference_or_pointer_kind * expression
  14. | ShiftPointerCast of qual_type * qual_type * reference_or_pointer_kind * expression
  15. | FieldAccess of expression * string
  16. | ArrayAccess of expression * expression
  17. | Conditional of expression * expression * expression
  18. | Static_call of qualified_name * signature * funkind * expression list * tkind * bool
  19. | Virtual_call of qualified_name * signature * funkind * expression * expression list * Stdlib.Int64.t * inheritance list * inheritance list
  20. | Dynamic_call of funkind * expression * expression list
  21. | Lambda_call of expression * expression list * Stdlib.Int64.t
  22. | Temporary of string * qual_type * init_expr * bool
  23. | InitializerList of qual_type * init_expr
  24. | VAArg of expression * qual_type
  25. | Throw of expression option
  26. | GnuBody of statement list
  27. | LambdaExpr of lambda_overload_instance list * capture list
and capture =
  1. | Cap_id of string * qual_type * bool
  2. | Cap_this of bool
and case_statement =
  1. | Case of compilation_constant * statement list
  2. | Default of statement list
and init_expr =
  1. | Single_init of expression
  2. | Implicit_init
  3. | Compound_init of init_expr list
  4. | Union_init of string * qual_type * init_expr
  5. | Array_init of qualified_name * expression
and cond_statement =
  1. | CondExpression of expression
  2. | CondVarDecl of string * qual_type * init_expr
and init_declarator = {
  1. id_name : string;
  2. init_type : qual_type;
  3. init_val : init_expr option;
}
and init_statement =
  1. | INop
  2. | IExpression of expression
  3. | IVarDecl of init_declarator list
and incr_statement =
  1. | CNop
  2. | CExpression of expression
and catch_block = {
  1. typed_arg : arg_decl option;
  2. cbody : statement list;
}
and statement =
  1. | Nop of location
  2. | Return of location * expression option
  3. | Expression of location * expression
  4. | VirtualExpression of location * expression
  5. | Code_annot of location * code_annotation
  6. | Ghost_block of location * statement list
  7. | Block of location * statement list
  8. | Condition of location * cond_statement * statement * statement
  9. | Label of location * string
  10. | Goto of location * string
  11. | Switch of location * cond_statement * case_statement list
  12. | VarDecl of location * string * qual_type * init_expr option
  13. | Break of location
  14. | Continue of location
  15. | While of location * expression * statement * code_annotation list
  16. | DoWhile of location * expression * statement * code_annotation list
  17. | For of location * init_statement * expression option * incr_statement * statement * code_annotation list
  18. | TryCatch of location * statement list * catch_block list
  19. | GccInlineAsm of location * specifier list * string list * asm_details option
and asm_details = {
  1. outputs : asm_IO list;
  2. inputs : asm_IO list;
  3. clobbers : string list;
  4. ad_labels : string list;
}
and asm_IO = {
  1. aIO_name : string option;
  2. constraints : string;
  3. expr : expression;
}
and access_kind =
  1. | Public
  2. | Protected
  3. | Private
and inheritance = {
  1. base : qualified_name;
  2. templated_kind : tkind;
  3. access : access_kind;
  4. is_virtual : vkind;
  5. vmt_position : int;
}
and class_decl =
  1. | CMethod of location * string * funkind * qual_type * arg_decl list * bool * statement list option * bool * tkind * bool * qual_type list option * function_contract option
  2. | CCompound of location * string * ckind * inheritance list option * class_decl list option * tkind * bool
  3. | CFieldDecl of location * string * qual_type * int option * bool
  4. | CTypedef of location * string * qual_type
  5. | CStaticConst of location * string * ikind * ickind * Stdlib.Int64.t
  6. | CEnum of location * string * ikind * compilation_constant list option
  7. | Class_annot of location * global_annotation
and decl_or_impl_name =
  1. | Declaration of string
  2. | Implementation of qualified_name
and translation_unit_decl =
  1. | Function of decl_or_impl_name * funkind * location * qual_type * arg_decl list * statement list option * bool * bool * bool * tkind * bool * qual_type list option * function_contract option
  2. | Compound of location * decl_or_impl_name * ckind * inheritance list option * class_decl list option * bool * tkind * bool * bool
  3. | GlobalVarDecl of location * decl_or_impl_name * qual_type * init_expr option * bool * bool
  4. | Typedef of location * decl_or_impl_name * qual_type * bool * bool
  5. | Namespace of location * string * translation_unit_decl list
  6. | StaticConst of location * string * ikind * ickind * Stdlib.Int64.t * bool * bool
  7. | EnumDecl of location * decl_or_impl_name * ikind * compilation_constant list option * bool * bool
  8. | GlobalAnnotation of location * global_annotation
and file = {
  1. filename : string;
  2. globals : translation_unit_decl list;
}
and logic_constant =
  1. | LCInt of string
  2. | LStr of string
  3. | LWStr of Stdlib.Int64.t list
  4. | LChr of int
  5. | LWChr of int
  6. | LCReal of string
  7. | LCEnum of Stdlib.Int64.t * qualified_name
and logic_type =
  1. | Lvoid
  2. | Linteger
  3. | Lreal
  4. | Lint of ikind
  5. | Lfloat of fkind
  6. | Larray of logic_type * logic_constant option
  7. | Lpointer of logic_type
  8. | Lreference of logic_type
  9. | Lenum of qualified_name
  10. | Lstruct of qualified_name * tkind
  11. | Lunion of qualified_name * tkind
  12. | LCnamed of qualified_name * bool
  13. | Lvariable of qualified_name
  14. | Lnamed of qualified_name * bool * logic_type list
  15. | Larrow of logic_type list * logic_type
and logic_label =
  1. | StmtLabel of string
  2. | LogicLabel of string
and term = {
  1. node : term_node;
  2. loc : location;
  3. names : string list;
}
and logic_label_pair = {
  1. fst : logic_label;
  2. snd : logic_label;
}
and term_node =
  1. | TConst of logic_constant
  2. | TLval of term_lval
  3. | TSizeOf of logic_type
  4. | TSizeOfStr of string
  5. | TUnOp of uokind * term
  6. | TBinOp of bokind * term * term
  7. | TCastE of logic_type * term
  8. | TAddrOf of term_lval
  9. | TStartOf of term_lval
  10. | TFieldAccess of term * term_offset
  11. | TFalse
  12. | TTrue
  13. | TApp of qualified_name * logic_label_pair list * term list * bool
  14. | TLambda of logic_var_def list * term
  15. | TDataCons of qualified_name * term list
  16. | TIf of term * term * term
  17. | TAt of term * logic_label
  18. | TBase_addr of logic_label option * term
  19. | TOffset of logic_label option * term
  20. | TBlock_length of logic_label option * term
  21. | TNull
  22. | TLogic_coerce of logic_type * term
  23. | TCoerce of term * logic_type
  24. | TCoerceE of term * term
  25. | TUpdate of term * term_offset * term
  26. | TEmpty_set
  27. | TUnion of term list
  28. | TInter of term list
  29. | TComprehension of term * logic_var_def list * predicate_named option
  30. | TRange of term option * term option
  31. | TLet of logic_info * term
and term_lval = {
  1. base_support : term_lhost;
  2. offset : term_offset;
}
and term_lhost =
  1. | TVar of logic_var
  2. | TCFun of qualified_name * signature
  3. | TResult of logic_type
  4. | TMem of term
and model_info = {
  1. model_name : string;
  2. field_type : logic_type;
  3. base_type : logic_type;
  4. decl : location;
}
and term_offset =
  1. | TNoOffset
  2. | TField of string * term_offset
  3. | TBase of qualified_name * tkind * term_offset
  4. | TVirtualBase of qualified_name * tkind * term_offset
  5. | TDerived of qualified_name * tkind * qualified_name * tkind * term_offset
  6. | TModel of string * term_offset
  7. | TIndex of term * term_offset
and logic_arg_decl = {
  1. la_type : logic_type;
  2. la_name : string;
}
and logic_info = {
  1. li_name : qualified_name;
  2. li_extern_c : bool;
  3. arg_labels : logic_label list;
  4. tparams : string list;
  5. returned_type : logic_type option;
  6. profile : logic_arg_decl list;
  7. fun_body : logic_body;
}
and inductive_definition = {
  1. def_name : string;
  2. labels : logic_label list;
  3. arguments : string list;
  4. def : predicate_named;
}
and logic_body =
  1. | LBnone
  2. | LBreads of term list
  3. | LBterm of term
  4. | LBpred of predicate_named
  5. | LBinductive of inductive_definition list
and logic_type_info = {
  1. type_name : qualified_name;
  2. logic_type_info_is_extern_c : bool;
  3. params : string list;
  4. definition : logic_type_def option;
}
and logic_type_def =
  1. | LTsum of logic_ctor_info list
  2. | LTsyn of logic_type
and logic_var_kind =
  1. | LVGlobal
  2. | LVCGlobal
  3. | LVCLocal
  4. | LVFormal
  5. | LVQuant
  6. | LVLocal
  7. | LVBuiltin
and logic_var_def = {
  1. logic_var_def_lv_name : qualified_name;
  2. lv_type : logic_type;
  3. logic_var_def_lv_kind : logic_var_kind;
}
and logic_var = {
  1. logic_var_lv_name : qualified_name;
  2. logic_var_lv_kind : logic_var_kind;
}
and logic_ctor_info = {
  1. ctor_name : qualified_name;
  2. logic_ctor_info_is_extern_c : bool;
  3. constype : qualified_name;
  4. ctor_params : logic_type list;
}
and relation =
  1. | Rlt
  2. | Rgt
  3. | Rle
  4. | Rge
  5. | Req
  6. | Rneq
and predicate =
  1. | Pfalse
  2. | Ptrue
  3. | PApp of qualified_name * logic_label_pair list * term list * bool
  4. | Pseparated of term list
  5. | Prel of relation * term * term
  6. | Pand of predicate_named * predicate_named
  7. | Por of predicate_named * predicate_named
  8. | Pxor of predicate_named * predicate_named
  9. | Pimplies of predicate_named * predicate_named
  10. | Piff of predicate_named * predicate_named
  11. | Pnot of predicate_named
  12. | Pif of term * predicate_named * predicate_named
  13. | Plet of logic_info * predicate_named
  14. | Pforall of logic_var_def list * predicate_named
  15. | Pexists of logic_var_def list * predicate_named
  16. | Pat of logic_label * predicate_named
  17. | Pvalid_function of term
  18. | Pvalid_read of logic_label option * term
  19. | Pvalid of logic_label option * term
  20. | Pinitialized of logic_label option * term
  21. | Pallocable of logic_label option * term
  22. | Pfreeable of logic_label option * term
  23. | Pfresh of logic_label option * logic_label option * term * term
  24. | Psubtype of term * term
and variant = {
  1. vbody : term;
  2. vname : string option;
}
and allocation =
  1. | FreeAlloc of term list * term list
  2. | FreeAllocAny
and deps =
  1. | From of term list
  2. | FromAny
and from = {
  1. floc : term;
  2. vars : deps;
}
and assigns =
  1. | WritesAny
  2. | Writes of from list
and function_contract = {
  1. behavior : behavior list;
  2. variant : variant option;
  3. terminates : predicate_named option;
  4. complete_behaviors : set_of_behaviors list;
  5. disjoint_behaviors : set_of_behaviors list;
}
and behavior = {
  1. beh_name : string;
  2. requires : predicate_named list;
  3. assumes : predicate_named list;
  4. post_cond : post_condition list;
  5. assignements : assigns;
  6. alloc : allocation;
  7. extended : behavior_extensions list;
}
and termination_kind =
  1. | Normal
  2. | Exits
  3. | Breaks
  4. | Continues
  5. | Returns
and loop_pragma =
  1. | Unroll_specs of term list
  2. | Widen_hints of term list
  3. | Widen_variables of term list
and slice_pragma =
  1. | SPexpr of term
  2. | SPctrl
  3. | SPstmt
and impact_pragma =
  1. | IPexpr of term
  2. | IPstmt
and pragma =
  1. | Loop_pragma of loop_pragma
  2. | Slice_pragma of slice_pragma
  3. | Impact_pragma of impact_pragma
and predicate_named = {
  1. pred_name : string list;
  2. pred_loc : location;
  3. pred_content : predicate;
}
and post_condition = {
  1. tkind : termination_kind;
  2. pred : predicate_named;
}
and behavior_extensions = {
  1. ext_name : string;
  2. identifier : int;
  3. predicates : predicate_named list;
}
and set_of_behaviors = {
  1. behaviors : string list;
}
and invariant_kind =
  1. | InvariantAsAssertion
  2. | NormalLoop
and code_annotation =
  1. | Assert of string list * predicate_named
  2. | StmtSpec of string list * function_contract
  3. | Invariant of string list * invariant_kind * predicate_named
  4. | Variant of variant
  5. | Assigns of string list * assigns
  6. | Allocation of string list * allocation
  7. | Pragma of pragma
and global_annotation =
  1. | Dfun_or_pred of location * logic_info
  2. | Dvolatile of location * term list * qualified_name option * qualified_name option
  3. | Daxiomatic of location * string * global_annotation list
  4. | Dtype of location * logic_type_info
  5. | Dlemma of location * string * bool * logic_label list * string list * predicate_named
  6. | Dinvariant of location * logic_info
  7. | Dtype_annot of location * logic_info
  8. | Dmodel_annot of location * model_info
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct