Lang.AstAST of the C language.
type c_typedef = {c_typedef_org_name : string;name as in source
*)c_typedef_unique_name : string;unique name
*)mutable c_typedef_def : MopsaLib.typ;declaration
*)c_typedef_range : Mopsa_utils.Core.Location.range;declaration location
*)}Type definition.
and c_record_type = {c_record_kind : c_record_kind;c_record_org_name : string;name as in source, may be empty
*)c_record_unique_name : string;unique, non-empty name
*)c_record_defined : bool;false if only declared
*)c_record_sizeof : Z.t;size of record, in bytes
*)c_record_alignof : Z.t;alignment, in bytes
*)mutable c_record_fields : c_record_field list;c_record_range : Mopsa_utils.Core.Location.range;declaration location
*)}Struct or union type.
and c_record_field = {c_field_org_name : string;may be empty for anonymous or padding fields
*)c_field_name : string;non-empty name
*)c_field_offset : int;c_field_bit_offset : int;c_field_type : MopsaLib.typ;c_field_range : Mopsa_utils.Core.Location.range;declaration location
*)c_field_index : int;}Struct or union field.
and c_enum_type = {c_enum_org_name : string;name as in source, may be empty
*)c_enum_unique_name : string;unique, non-empty name
*)c_enum_defined : bool;false if only declared
*)c_enum_values : c_enum_value list;c_enum_integer_type : c_integer_type;c_enum_range : Mopsa_utils.Core.Location.range;declaration location
*)}Enumerated type.
and c_enum_value = {c_enum_val_org_name : string;name as in source
*)c_enum_val_unique_name : string;unique name
*)c_enum_val_value : Z.t;c_enum_val_range : MopsaLib.range;}A possible value in an enumerated type.
and c_array_length = | C_array_no_length| C_array_length_cst of Z.t| C_array_length_expr of MopsaLib.exprCases of arrays length.
*)Type qualifiers.
and c_function_type = {c_ftype_return : MopsaLib.typ;c_ftype_params : MopsaLib.typ list;c_ftype_variadic : bool;}Function type.
type MopsaLib.typ += | T_c_voidVoid type.
*)| T_c_bool| T_c_integer of c_integer_type| T_c_float of c_float_type| T_c_pointer of MopsaLib.typScalar types.
*)| T_c_array of MopsaLib.typ * c_array_lengthArrays.
*)| T_c_bitfield of MopsaLib.typ * intBitfields, with bit-width, only used in struct.
*)| T_c_function of c_function_type optionFunction, with or without a prototype
*)| T_c_builtin_fnBuilt-in functions
*)| T_c_typedef of c_typedefTypedefs
*)| T_c_record of c_record_typestruct and union
*)| T_c_enum of c_enum_typeenums
*)| T_c_qualified of c_qual * MopsaLib.typQualified type.
*)| T_c_block_object of MopsaLib.typType of block objects.
*)| T_c_unknown_builtin of stringUnknown builtin type.
*)***********************
type c_fundec = {mutable c_func_uid : int;unique identifier
*)mutable c_func_org_name : string;original name
*)mutable c_func_unique_name : string;unique name for globals and statics
*)c_func_is_static : bool;mutable c_func_return : MopsaLib.typ;type of returned value
*)mutable c_func_parameters : MopsaLib.var list;function parameters
*)mutable c_func_body : MopsaLib.stmt option;function body
*)mutable c_func_static_vars : MopsaLib.var list;static variables declared in the function
*)mutable c_func_local_vars : MopsaLib.var list;local variables declared in the function (excluding parameters)
*)mutable c_func_variadic : bool;whether the has a variable number of arguments
*)mutable c_func_range : MopsaLib.range;location range of the declaration
*)mutable c_func_name_range : MopsaLib.range;location range of the name in the declaration
*)mutable c_func_stub : Stubs.Ast.stub_func option;stub comment
*)}Function descriptor.
type c_var_scope = | Variable_globalglobal shared among translation units
*)| Variable_externdeclared but not defined
*)| Variable_local of c_fundeclocal to a function
*)| Variable_parameter of c_fundecformal argument
*)| Variable_file_static of stringrestricted to a translation unit
*)| Variable_func_static of c_fundecrestricted to a function
*)val pp_scope : Format.formatter -> c_var_scope -> unittype c_var_init = | C_init_expr of MopsaLib.expr| C_init_list of c_var_init list * c_var_init optionfiller
*)| C_init_implicit of MopsaLib.typVariable initialization.
type cvar = {cvar_scope : c_var_scope;life-time scope of the variable
*)cvar_range : MopsaLib.range;declaration range
*)cvar_uid : int;cvar_orig_name : string;cvar_uniq_name : string;cvar_before_stmts : MopsaLib.stmt list;list of statements to execute before the declaration of a variable
*)cvar_after_stmts : MopsaLib.stmt list;list of statements to execute after the declaration of a variable
*)}type MopsaLib.constant += | C_c_character of Z.t * c_character_kindConstant character
*)| C_c_string of string * c_character_kindConstant string literal
*)| C_c_invalidInvalid pointer value
*)type MopsaLib.expr_kind += | E_c_conditional of MopsaLib.expr * MopsaLib.expr * MopsaLib.exprelse
*)| E_c_array_subscript of MopsaLib.expr * MopsaLib.exprindex
*)| E_c_member_access of MopsaLib.expr * int * stringfield
*)| E_c_function of c_fundec| E_c_builtin_function of string| E_c_builtin_call of string * MopsaLib.expr list| E_c_arrow_access of MopsaLib.expr * int * stringfield
*)| E_c_assign of MopsaLib.expr * MopsaLib.exprrvalue
*)| E_c_compound_assign of MopsaLib.expr
* MopsaLib.typ
* MopsaLib.operator
* MopsaLib.expr
* MopsaLib.typtype of the result, before converting back to lvalue type
*)| E_c_comma of MopsaLib.expr * MopsaLib.expr, operator
*)| E_c_increment of c_inc_direction * c_inc_location * MopsaLib.expr| E_c_address_of of MopsaLib.expr& operator (address of lvalue)
*)| E_c_deref of MopsaLib.expr* operator (pointer dereference)
*)| E_c_cast of MopsaLib.expr * boolexplicitness
*)| E_c_statement of MopsaLib.stmt| E_c_predefined of stringpredefined identifier
*)| E_c_var_args of MopsaLib.expr__builtin_va_arg
*)| E_c_atomic of int * MopsaLib.expr * MopsaLib.expr| E_c_block_object of MopsaLib.exprBlock objects are useful to distinguish between operations on the block itself and its content. For, expanding the contents of a block will duplicate every cell in the block, while expanding the block object will update the pointers that point to the block.
*)type c_scope_update = {c_scope_var_added : MopsaLib.var list;c_scope_var_removed : MopsaLib.var list;}Scope update information for jump statements
type MopsaLib.stmt_kind += | S_c_goto_stab of MopsaLib.stmtstabilization point for goto statement
*)| S_c_declaration of MopsaLib.var * c_var_init option * c_var_scopedeclaration of a variable
*)| S_c_do_while of MopsaLib.stmt * MopsaLib.exprcondition
*)| S_c_for of MopsaLib.stmt
* MopsaLib.expr option
* MopsaLib.expr option
* MopsaLib.stmtbody
*)| S_c_return of MopsaLib.expr option * c_scope_updatereturn statement
*)| S_c_break of c_scope_updatebreak statement
*)| S_c_continue of c_scope_updatecontinue statement
*)| S_c_goto of string * c_scope_updategoto statements.
*)| S_c_switch of MopsaLib.expr * MopsaLib.stmtswitch statement.
*)| S_c_label of stringstatement label.
*)| S_c_switch_case of MopsaLib.expr list * c_scope_updatecase of a switch statement.
case a: case b: stmt;
is represented through S_c_switch_case a; b to factor in some cases
For integer cases, we use the interval a, b to simplify expressions, similar to the GCC C extension for ranges
| S_c_switch_default of c_scope_updatedefault case of switch statements.
*)| S_c_asm of stringinline assembly for now, we keep only a string representation to display warnings; see C_AST.asm_kind for a more usable representation when support is added
*)type c_program = {c_globals : (MopsaLib.var * c_var_init option) list;global variables of the program
*)c_functions : c_fundec list;functions of the program
*)c_stub_directives : Stubs.Ast.stub_directive list;list of stub directives
*)}module CProgramKey : sig ... endval c_program_ctx :
('a, c_program) Mopsa_analyzer__Framework__Core__Context.ctx_keyFlow-insensitive context to keep the analyzed C program
val set_c_program :
c_program ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Mopsa_analyzer.MopsaLib.Flow.flowSet the C program in the flow
val get_c_program : 'a Mopsa_analyzer.MopsaLib.Flow.flow -> c_programGet the C program from the flow
val to_clang_int_type : c_integer_type -> Mopsa_c_parser.C_AST.integer_typeval to_clang_float_type : c_float_type -> Mopsa_c_parser.C_AST.float_typeval from_clang_int_type : Mopsa_c_parser.C_AST.integer_type -> c_integer_typeval from_clang_float_type : Mopsa_c_parser.C_AST.float_type -> c_float_typeTarget information
module TargetCtx : sig ... endval get_c_target_info :
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
Mopsa_c_parser.Clang_AST.target_infoval set_c_target_info :
Mopsa_c_parser.Clang_AST.target_info ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Mopsa_analyzer.MopsaLib.Flow.flowval remove_c_target_info :
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Mopsa_analyzer.MopsaLib.Flow.flowval sizeof_type_in_target :
MopsaLib.typ ->
Mopsa_c_parser.C_utils.C.target_info ->
Z.tsizeof t computes the size (in bytes) of a C type t
val sizeof_type : MopsaLib.typ -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> Z.tval host_target_info : Mopsa_c_parser.Clang_AST.target_infoval sizeof_type_in_host : MopsaLib.typ -> Z.tval sizeof_expr :
MopsaLib.typ ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprSize (in bytes) of a type, as an expression. Handles variable-length ararys.
val remove_typedef : MopsaLib.typ -> MopsaLib.typval remove_qual : MopsaLib.typ -> MopsaLib.typval remove_typedef_qual : MopsaLib.typ -> MopsaLib.typval is_signed : MopsaLib.typ -> boolis_signed t whether t is signed
val rangeof : MopsaLib.typ -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> Z.t * Z.trange t computes the interval range of type t
val int_rangeof :
MopsaLib.typ ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
int * intrange t computes the interval range of type t as integers
val wrap_expr :
MopsaLib.expr ->
(Z.t * Z.t) ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprwrap_expr e (l,h) expression needed to bring back e in range (l,h)
val is_c_char_type : MopsaLib.typ -> boolval is_c_string_type : MopsaLib.typ -> boolval is_c_int_type : MopsaLib.typ -> boolis_c_int_type t tests whether t is an integer type
val is_c_int_array_type : MopsaLib.typ -> boolval is_c_signed_int_type : MopsaLib.typ -> boolval is_c_bool_type : MopsaLib.typ -> boolval is_c_float_type : MopsaLib.typ -> boolis_c_int_type t tests whether t is a floating point type
val get_c_float_type : MopsaLib.typ -> c_float_typeval get_c_float_precision : MopsaLib.typ -> Universal.Lang.Ast.float_precGet the float precision from a C type
val is_c_bitfield : MopsaLib.typ -> boolval is_c_num_type : MopsaLib.typ -> boolis_c_int_type t tests whether t is a numeric type
val is_c_scalar_type : MopsaLib.typ -> boolis_c_scalar_type t tests whether t is a scalar type
val is_c_pointer_type : MopsaLib.typ -> boolis_c_pointer t tests whether t is a pointer
val is_c_void_type : MopsaLib.typ -> boolval is_c_record_type : MopsaLib.typ -> boolval is_c_struct_type : MopsaLib.typ -> boolval is_c_union_type : MopsaLib.typ -> boolval is_c_array_type : MopsaLib.typ -> boolval is_c_function_type : MopsaLib.typ -> boolval pointer_type : MopsaLib.typ -> MopsaLib.typis_scalartype t lifts t to a pointer to t
val under_pointer_type : MopsaLib.typ -> MopsaLib.typval under_array_type : MopsaLib.typ -> MopsaLib.typval under_type : MopsaLib.typ -> MopsaLib.typval void_to_char : MopsaLib.typ -> MopsaLib.typval get_array_constant_length : MopsaLib.typ -> Z.tval align_byte : MopsaLib.typ -> int -> intval is_c_type : MopsaLib.typ -> boolval is_c_function_parameter : MopsaLib.var -> boolval mk_c_address_of :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_deref :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_member_access :
MopsaLib.expr ->
c_record_field ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_arrow_access :
MopsaLib.expr ->
c_record_field ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_member_access_by_name :
MopsaLib.expr ->
string ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_arrow_access_by_name :
MopsaLib.expr ->
string ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_subscript_access :
MopsaLib.expr ->
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_character :
char ->
Mopsa_utils.Core.Location.range ->
MopsaLib.typ ->
MopsaLib.exprval extract_multibyte_integer :
string ->
int ->
MopsaLib.typ ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
Z.tval mk_c_multibyte_integer :
string ->
int ->
MopsaLib.typ ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_invalid_pointer : Mopsa_utils.Core.Location.range -> MopsaLib.exprval void : MopsaLib.typval u8 : MopsaLib.typval s8 : MopsaLib.typval s16 : MopsaLib.typval u16 : MopsaLib.typval s32 : MopsaLib.typval u32 : MopsaLib.typval s64 : MopsaLib.typval u64 : MopsaLib.typval ul : MopsaLib.typval sl : MopsaLib.typval ull : MopsaLib.typval sll : MopsaLib.typval array_type : MopsaLib.typ -> Z.t -> MopsaLib.typval size_type : 'a Mopsa_analyzer.MopsaLib.Flow.flow -> MopsaLib.typval type_of_string : string -> MopsaLib.typval is_c_block_object_type : MopsaLib.typ -> boolval to_c_block_object : MopsaLib.expr -> MopsaLib.exprval of_c_block_object : MopsaLib.expr -> MopsaLib.exprval mk_c_string :
?kind:c_character_kind ->
string ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_fun_typ : c_fundec -> MopsaLib.typval mk_c_call :
c_fundec ->
MopsaLib.expr list ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_builtin_call :
string ->
MopsaLib.expr list ->
Framework.Core.Ast.Typ.typ ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_call_stmt :
c_fundec ->
MopsaLib.expr list ->
Mopsa_utils.Core.Location.range ->
MopsaLib.stmtval mk_c_cast :
?esynthetic:bool ->
MopsaLib.expr ->
Framework.Core.Ast.Typ.typ ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_null :
?esynthetic:bool ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval mk_c_declaration :
MopsaLib.var ->
c_var_init option ->
c_var_scope ->
Mopsa_utils.Core.Location.range ->
MopsaLib.stmtval is_c_global_scope : c_var_scope -> boolval find_c_record_field : int -> MopsaLib.typ -> c_record_fieldStatement comparison *
val compare_c_var_init : c_var_init -> c_var_init -> intval compare_c_var_scope : c_var_scope -> c_var_scope -> intval compare_c_var_scope_update : c_scope_update -> c_scope_update -> intval range_cond :
MopsaLib.expr ->
Z.t ->
Z.t ->
Mopsa_utils.Core.Location.range ->
MopsaLib.exprval remove_casts : MopsaLib.expr -> MopsaLib.exprval c_expr_to_z :
MopsaLib.expr ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
Z.t optionSimplify C constant expressions to constants
val is_c_expr_equals_z :
MopsaLib.expr ->
Z.t ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
boolval is_c_constant :
MopsaLib.expr ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
boolval is_c_lval : MopsaLib.expr -> boolval is_c_deref : MopsaLib.expr -> boolval get_c_deref_type : MopsaLib.expr -> MopsaLib.typval is_c_variable_length_array_type : MopsaLib.typ -> boolCheck if v is declared as a variable length array
val is_c_no_length_array_type : MopsaLib.typ -> boolCheck if v is declared as an array without length (as for many auxiliary variables)
val find_c_fundec_by_name :
string ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
c_fundecFind the definition of a C function
val find_c_fundec_by_uid :
int ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
c_fundecval assert_valid_string :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postCheck if a pointer points to a nul-terminated array
val assert_valid_wide_string :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postCheck if a pointer points to a nul-terminated wide char array
val assert_valid_stream :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postCheck if a pointer points to a valid stream
val assert_valid_file_descriptor :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postCheck if a pointer points to a valid file descriptor
val assert_valid_ptr :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postCheck if a pointer is valid
val memrand :
MopsaLib.expr ->
MopsaLib.expr ->
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postRandomize an entire array
val strrand :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postRandomize a string
val strnrand :
MopsaLib.expr ->
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postRandomize a substring
val wcsnrand :
MopsaLib.expr ->
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postRandomize a wide substring
val memset :
MopsaLib.expr ->
MopsaLib.expr ->
MopsaLib.expr ->
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postSet elements of an array with the same value c
val memcpy :
MopsaLib.expr ->
MopsaLib.expr ->
MopsaLib.expr ->
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postCopy elements of an array
val error_error :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postExit if status is non-zero
val error_error_at_line :
MopsaLib.expr ->
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Core.Post.postExit if status is non-zero
val asprintf_stub :
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Framework.Core.Eval.evalval vasprintf_stub :
bool ->
MopsaLib.expr ->
MopsaLib.expr ->
Mopsa_utils.Core.Location.range ->
('a, 'b) MopsaLib.man ->
'a Mopsa_analyzer.MopsaLib.Flow.flow ->
'a Framework.Core.Eval.evalval var_scope : MopsaLib.var -> c_var_scope