Lang.AstSourceAST 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 : Mopsa.typ;declaration
*)c_typedef_range : Mopsa.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.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 : Mopsa.typ;c_field_range : Mopsa.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.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 : Mopsa.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 Mopsa.exprCases of arrays length.
*)Type qualifiers.
Function type.
type Mopsa.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 Mopsa.typScalar types.
*)| T_c_array of Mopsa.typ * c_array_lengthArrays.
*)| T_c_bitfield of Mopsa.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 * Mopsa.typQualified type.
*)| T_c_block_object of Mopsa.typType of block objects.
*)***********************
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 : Mopsa.typ;type of returned value
*)mutable c_func_parameters : Mopsa.var list;function parameters
*)mutable c_func_body : Mopsa.stmt option;function body
*)mutable c_func_static_vars : Mopsa.var list;static variables declared in the function
*)mutable c_func_local_vars : Mopsa.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 : Mopsa.range;location range of the declaration
*)mutable c_func_name_range : Mopsa.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
*)type c_var_init = | C_init_expr of Mopsa.expr| C_init_list of c_var_init list * c_var_init optionfiller
*)| C_init_implicit of Mopsa.typVariable initialization.
type cvar = {cvar_scope : c_var_scope;life-time scope of the variable
*)cvar_range : Mopsa.range;declaration range
*)cvar_uid : int;cvar_orig_name : string;cvar_uniq_name : string;}type Mopsa.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 Mopsa.expr_kind += | E_c_conditional of Mopsa.expr * Mopsa.expr * Mopsa.exprelse
*)| E_c_array_subscript of Mopsa.expr * Mopsa.exprindex
*)| E_c_member_access of Mopsa.expr * int * stringfield
*)| E_c_function of c_fundec| E_c_builtin_function of string| E_c_builtin_call of string * Mopsa.expr list| E_c_arrow_access of Mopsa.expr * int * stringfield
*)| E_c_assign of Mopsa.expr * Mopsa.exprrvalue
*)| E_c_compound_assign of Mopsa.expr
* Mopsa.typ
* Mopsa.operator
* Mopsa.expr
* Mopsa.typtype of the result, before converting back to lvalue type
*)| E_c_comma of Mopsa.expr * Mopsa.expr, operator
*)| E_c_increment of c_inc_direction * c_inc_location * Mopsa.expr| E_c_address_of of Mopsa.expr& operator (address of lvalue)
*)| E_c_deref of Mopsa.expr* operator (pointer dereference)
*)| E_c_cast of Mopsa.expr * boolexplicitness
*)| E_c_statement of Mopsa.stmt| E_c_predefined of stringpredefined identifier
*)| E_c_var_args of Mopsa.expr__builtin_va_arg
*)| E_c_atomic of int * Mopsa.expr * Mopsa.expr| E_c_block_object of Mopsa.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.
*)Scope update information for jump statements
type Mopsa.stmt_kind += | S_c_goto_stab of Mopsa.stmtstabilization point for goto statement
*)| S_c_declaration of Mopsa.var * c_var_init option * c_var_scopedeclaration of a variable
*)| S_c_do_while of Mopsa.stmt * Mopsa.exprcondition
*)| S_c_for of Mopsa.stmt * Mopsa.expr option * Mopsa.expr option * Mopsa.stmtbody
*)| S_c_return of Mopsa.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 Mopsa.expr * Mopsa.stmtswitch statement.
*)| S_c_label of stringstatement label.
*)| S_c_switch_case of Mopsa.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 : (Mopsa.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 ... endFlow-insensitive context to keep the analyzed C program
Set the C program in the flow
Get the C program from the flow
Target information
module TargetCtx : sig ... endval set_c_target_info :
Mopsa_c_parser.Clang_AST.target_info ->
'a Mopsa.Flow.flow ->
'a Mopsa.Flow.flowsizeof t computes the size (in bytes) of a C type t
Size (in bytes) of a type, as an expression. Handles variable-length ararys.
range t computes the interval range of type t
range t computes the interval range of type t as integers
wrap_expr e (l,h) expression needed to bring back e in range (l,h)
is_c_int_type t tests whether t is a floating point type
Get the float precision from a C type
val mk_c_member_access :
Mopsa.expr ->
c_record_field ->
Mopsa_utils.Location.range ->
Mopsa.exprval mk_c_arrow_access :
Mopsa.expr ->
c_record_field ->
Mopsa_utils.Location.range ->
Mopsa.exprval mk_c_member_access_by_name :
Mopsa.expr ->
string ->
Mopsa_utils.Location.range ->
Mopsa.exprval mk_c_arrow_access_by_name :
Mopsa.expr ->
string ->
Mopsa_utils.Location.range ->
Mopsa.exprval mk_c_subscript_access :
Mopsa.expr ->
Mopsa.expr ->
Mopsa_utils.Location.range ->
Mopsa.exprval mk_c_multibyte_integer :
string ->
int ->
Mopsa.typ ->
'a Mopsa.Flow.flow ->
Mopsa_utils.Location.range ->
Mopsa.exprval mk_c_string :
?kind:c_character_kind ->
string ->
Mopsa_utils.Location.range ->
Mopsa.exprval mk_c_builtin_call :
string ->
Mopsa.expr list ->
Ast.Typ.typ ->
Mopsa_utils.Location.range ->
Mopsa.exprval mk_c_declaration :
Mopsa.var ->
c_var_init option ->
c_var_scope ->
Mopsa_utils.Location.range ->
Mopsa.stmtStatement comparison *
Simplify C constant expressions to constants
Check if v is declared as a variable length array
Check if v is declared as an array without length (as for many auxiliary variables)
Find the definition of a C function
val assert_valid_string :
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postCheck if a pointer points to a nul-terminated array
val assert_valid_wide_string :
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postCheck if a pointer points to a nul-terminated wide char array
val assert_valid_stream :
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postCheck if a pointer points to a valid stream
val assert_valid_file_descriptor :
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postCheck if a pointer points to a valid file descriptor
val assert_valid_ptr :
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postCheck if a pointer is valid
val memrand :
Mopsa.expr ->
Mopsa.expr ->
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postRandomize an entire array
val strrand :
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postRandomize a string
val strnrand :
Mopsa.expr ->
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postRandomize a substring
val wcsnrand :
Mopsa.expr ->
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postRandomize a wide substring
val memset :
Mopsa.expr ->
Mopsa.expr ->
Mopsa.expr ->
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postSet elements of an array with the same value c
val memcpy :
Mopsa.expr ->
Mopsa.expr ->
Mopsa.expr ->
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postCopy elements of an array
val error_error :
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postExit if status is non-zero
val error_error_at_line :
Mopsa.expr ->
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Post.postExit if status is non-zero
val asprintf_stub :
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Eval.evalval vasprintf_stub :
bool ->
Mopsa.expr ->
Mopsa.expr ->
Mopsa_utils.Location.range ->
('a, 'b) Mopsa.man ->
'a Mopsa.Flow.flow ->
'a Core.Eval.evalStack variables
This vkind is used to attach the callstack to local variables
Create a stack variable