package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

mopsa.lip6.fr Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.2.tar.gz
md5=37966e98ffeebcedc09bd6e9b2b81f69
sha512=40d4d826c25f680766c07eccbabdf5e8a4fa023016e8a164e4e4f6b3781c8484dc4df437055721dfd19b9db8fb7fe3b61236c4833186d346fc7204a68d01eaaa

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/C/Lang/Ast/index.html

Module Lang.Ast

AST of the C language.

Types

type c_typedef = {
  1. c_typedef_org_name : string;
    (*

    name as in source

    *)
  2. c_typedef_unique_name : string;
    (*

    unique name

    *)
  3. mutable c_typedef_def : MopsaLib.typ;
    (*

    declaration

    *)
  4. c_typedef_range : Mopsa_utils.Core.Location.range;
    (*

    declaration location

    *)
}

Type definition.

and c_record_kind =
  1. | C_struct
  2. | C_union
    (*

    Whether a record is struct or union.

    *)
and c_record_type = {
  1. c_record_kind : c_record_kind;
  2. c_record_org_name : string;
    (*

    name as in source, may be empty

    *)
  3. c_record_unique_name : string;
    (*

    unique, non-empty name

    *)
  4. c_record_defined : bool;
    (*

    false if only declared

    *)
  5. c_record_sizeof : Z.t;
    (*

    size of record, in bytes

    *)
  6. c_record_alignof : Z.t;
    (*

    alignment, in bytes

    *)
  7. mutable c_record_fields : c_record_field list;
  8. c_record_range : Mopsa_utils.Core.Location.range;
    (*

    declaration location

    *)
}

Struct or union type.

and c_record_field = {
  1. c_field_org_name : string;
    (*

    may be empty for anonymous or padding fields

    *)
  2. c_field_name : string;
    (*

    non-empty name

    *)
  3. c_field_offset : int;
  4. c_field_bit_offset : int;
  5. c_field_type : MopsaLib.typ;
  6. c_field_range : Mopsa_utils.Core.Location.range;
    (*

    declaration location

    *)
  7. c_field_index : int;
}

Struct or union field.

and c_enum_type = {
  1. c_enum_org_name : string;
    (*

    name as in source, may be empty

    *)
  2. c_enum_unique_name : string;
    (*

    unique, non-empty name

    *)
  3. c_enum_defined : bool;
    (*

    false if only declared

    *)
  4. c_enum_values : c_enum_value list;
  5. c_enum_integer_type : c_integer_type;
  6. c_enum_range : Mopsa_utils.Core.Location.range;
    (*

    declaration location

    *)
}

Enumerated type.

and c_enum_value = {
  1. c_enum_val_org_name : string;
    (*

    name as in source

    *)
  2. c_enum_val_unique_name : string;
    (*

    unique name

    *)
  3. c_enum_val_value : Z.t;
  4. c_enum_val_range : MopsaLib.range;
}

A possible value in an enumerated type.

and c_integer_type =
  1. | C_signed_char
  2. | C_unsigned_char
  3. | C_signed_short
  4. | C_unsigned_short
  5. | C_signed_int
  6. | C_unsigned_int
  7. | C_signed_long
  8. | C_unsigned_long
  9. | C_signed_long_long
  10. | C_unsigned_long_long
  11. | C_signed_int128
  12. | C_unsigned_int128
    (*

    Integer types.

    *)
and c_float_type =
  1. | C_float
  2. | C_double
  3. | C_long_double
  4. | C_float128
  5. | C_float16
    (*

    Floating-point types.

    *)
and c_array_length =
  1. | C_array_no_length
  2. | C_array_length_cst of Z.t
  3. | C_array_length_expr of MopsaLib.expr
    (*

    Cases of arrays length.

    *)
and c_qual = {
  1. c_qual_is_const : bool;
  2. c_qual_is_volatile : bool;
  3. c_qual_is_restrict : bool;
}

Type qualifiers.

and c_function_type = {
  1. c_ftype_return : MopsaLib.typ;
  2. c_ftype_params : MopsaLib.typ list;
  3. c_ftype_variadic : bool;
}

Function type.

type MopsaLib.typ +=
  1. | T_c_void
    (*

    Void type.

    *)
  2. | T_c_bool
  3. | T_c_integer of c_integer_type
  4. | T_c_float of c_float_type
  5. | T_c_pointer of MopsaLib.typ
    (*

    Scalar types.

    *)
  6. | T_c_array of MopsaLib.typ * c_array_length
    (*

    Arrays.

    *)
  7. | T_c_bitfield of MopsaLib.typ * int
    (*

    Bitfields, with bit-width, only used in struct.

    *)
  8. | T_c_function of c_function_type option
    (*

    Function, with or without a prototype

    *)
  9. | T_c_builtin_fn
    (*

    Built-in functions

    *)
  10. | T_c_typedef of c_typedef
    (*

    Typedefs

    *)
  11. | T_c_record of c_record_type
    (*

    struct and union

    *)
  12. | T_c_enum of c_enum_type
    (*

    enums

    *)
  13. | T_c_qualified of c_qual * MopsaLib.typ
    (*

    Qualified type.

    *)
  14. | T_c_block_object of MopsaLib.typ
    (*

    Type of block objects.

    *)
  15. | T_c_unknown_builtin of string
    (*

    Unknown builtin type.

    *)

Function descriptor

***********************

type c_fundec = {
  1. mutable c_func_uid : int;
    (*

    unique identifier

    *)
  2. mutable c_func_org_name : string;
    (*

    original name

    *)
  3. mutable c_func_unique_name : string;
    (*

    unique name for globals and statics

    *)
  4. c_func_is_static : bool;
  5. mutable c_func_return : MopsaLib.typ;
    (*

    type of returned value

    *)
  6. mutable c_func_parameters : MopsaLib.var list;
    (*

    function parameters

    *)
  7. mutable c_func_body : MopsaLib.stmt option;
    (*

    function body

    *)
  8. mutable c_func_static_vars : MopsaLib.var list;
    (*

    static variables declared in the function

    *)
  9. mutable c_func_local_vars : MopsaLib.var list;
    (*

    local variables declared in the function (excluding parameters)

    *)
  10. mutable c_func_variadic : bool;
    (*

    whether the has a variable number of arguments

    *)
  11. mutable c_func_range : MopsaLib.range;
    (*

    location range of the declaration

    *)
  12. mutable c_func_name_range : MopsaLib.range;
    (*

    location range of the name in the declaration

    *)
  13. mutable c_func_stub : Stubs.Ast.stub_func option;
    (*

    stub comment

    *)
}

Function descriptor.

C variables

type c_var_scope =
  1. | Variable_global
    (*

    global shared among translation units

    *)
  2. | Variable_extern
    (*

    declared but not defined

    *)
  3. | Variable_local of c_fundec
    (*

    local to a function

    *)
  4. | Variable_parameter of c_fundec
    (*

    formal argument

    *)
  5. | Variable_file_static of string
    (*

    restricted to a translation unit

    *)
  6. | Variable_func_static of c_fundec
    (*

    restricted to a function

    *)
val pp_scope : Format.formatter -> c_var_scope -> unit
type c_var_init =
  1. | C_init_expr of MopsaLib.expr
  2. | C_init_list of c_var_init list * c_var_init option
    (*

    filler

    *)
  3. | C_init_implicit of MopsaLib.typ

Variable initialization.

type cvar = {
  1. cvar_scope : c_var_scope;
    (*

    life-time scope of the variable

    *)
  2. cvar_range : MopsaLib.range;
    (*

    declaration range

    *)
  3. cvar_uid : int;
  4. cvar_orig_name : string;
  5. cvar_uniq_name : string;
  6. cvar_before_stmts : MopsaLib.stmt list;
    (*

    list of statements to execute before the declaration of a variable

    *)
  7. cvar_after_stmts : MopsaLib.stmt list;
    (*

    list of statements to execute after the declaration of a variable

    *)
}
type MopsaLib.var_kind +=
  1. | V_cvar of cvar
    (*

    C variable

    *)

C expressions

type MopsaLib.operator +=
  1. | O_c_and
  2. | O_c_or
type c_inc_location =
  1. | PRE
  2. | POST
    (*

    Whether an incrementation is performed before (PRE) or after (POST) the expression value is used

    *)
type c_inc_direction =
  1. | INC
  2. | DEC
    (*

    Whether an incrementation is ++ or --

    *)
type c_character_kind =
  1. | C_char_ascii
  2. | C_char_wide
  3. | C_char_utf8
  4. | C_char_utf16
  5. | C_char_utf32
  6. | C_char_unevaluated
type MopsaLib.constant +=
  1. | C_c_character of Z.t * c_character_kind
    (*

    Constant character

    *)
  2. | C_c_string of string * c_character_kind
    (*

    Constant string literal

    *)
  3. | C_c_invalid
    (*

    Invalid pointer value

    *)
type MopsaLib.expr_kind +=
  1. | E_c_conditional of MopsaLib.expr * MopsaLib.expr * MopsaLib.expr
    (*

    else

    *)
  2. | E_c_array_subscript of MopsaLib.expr * MopsaLib.expr
    (*

    index

    *)
  3. | E_c_member_access of MopsaLib.expr * int * string
    (*

    field

    *)
  4. | E_c_function of c_fundec
  5. | E_c_builtin_function of string
  6. | E_c_builtin_call of string * MopsaLib.expr list
  7. | E_c_arrow_access of MopsaLib.expr * int * string
    (*

    field

    *)
  8. | E_c_assign of MopsaLib.expr * MopsaLib.expr
    (*

    rvalue

    *)
  9. | E_c_compound_assign of MopsaLib.expr * MopsaLib.typ * MopsaLib.operator * MopsaLib.expr * MopsaLib.typ
    (*

    type of the result, before converting back to lvalue type

    *)
  10. | E_c_comma of MopsaLib.expr * MopsaLib.expr
    (*

    , operator

    *)
  11. | E_c_increment of c_inc_direction * c_inc_location * MopsaLib.expr
  12. | E_c_address_of of MopsaLib.expr
    (*

    & operator (address of lvalue)

    *)
  13. | E_c_deref of MopsaLib.expr
    (*

    * operator (pointer dereference)

    *)
  14. | E_c_cast of MopsaLib.expr * bool
    (*

    explicitness

    *)
  15. | E_c_statement of MopsaLib.stmt
  16. | E_c_predefined of string
    (*

    predefined identifier

    *)
  17. | E_c_var_args of MopsaLib.expr
    (*

    __builtin_va_arg

    *)
  18. | E_c_atomic of int * MopsaLib.expr * MopsaLib.expr
  19. | E_c_block_object of MopsaLib.expr
    (*

    Block 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

type c_scope_update = {
  1. c_scope_var_added : MopsaLib.var list;
  2. c_scope_var_removed : MopsaLib.var list;
}

Scope update information for jump statements

Statements

type MopsaLib.stmt_kind +=
  1. | S_c_goto_stab of MopsaLib.stmt
    (*

    stabilization point for goto statement

    *)
  2. | S_c_declaration of MopsaLib.var * c_var_init option * c_var_scope
    (*

    declaration of a variable

    *)
  3. | S_c_do_while of MopsaLib.stmt * MopsaLib.expr
    (*

    condition

    *)
  4. | S_c_for of MopsaLib.stmt * MopsaLib.expr option * MopsaLib.expr option * MopsaLib.stmt
    (*

    body

    *)
  5. | S_c_return of MopsaLib.expr option * c_scope_update
    (*

    return statement

    *)
  6. | S_c_break of c_scope_update
    (*

    break statement

    *)
  7. | S_c_continue of c_scope_update
    (*

    continue statement

    *)
  8. | S_c_goto of string * c_scope_update
    (*

    goto statements.

    *)
  9. | S_c_switch of MopsaLib.expr * MopsaLib.stmt
    (*

    switch statement.

    *)
  10. | S_c_label of string
    (*

    statement label.

    *)
  11. | S_c_switch_case of MopsaLib.expr list * c_scope_update
    (*

    case 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

    *)
  12. | S_c_switch_default of c_scope_update
    (*

    default case of switch statements.

    *)
  13. | S_c_asm of string
    (*

    inline 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 = {
  1. c_globals : (MopsaLib.var * c_var_init option) list;
    (*

    global variables of the program

    *)
  2. c_functions : c_fundec list;
    (*

    functions of the program

    *)
  3. c_stub_directives : Stubs.Ast.stub_directive list;
    (*

    list of stub directives

    *)
}
type MopsaLib.prog_kind +=
  1. | C_program of c_program
module CProgramKey : sig ... end
val c_program_ctx : ('a, c_program) Mopsa_analyzer__Framework__Core__Context.ctx_key

Flow-insensitive context to keep the analyzed C program

Set the C program in the flow

Get the C program from the flow

Conversion to/from Clang parser types

val to_clang_float_type : c_float_type -> Mopsa_c_parser.C_AST.float_type
val from_clang_float_type : Mopsa_c_parser.C_AST.float_type -> c_float_type

Target information

module TargetCtx : sig ... end

Sizes and alignments

val sizeof_type_in_target : MopsaLib.typ -> Mopsa_c_parser.C_utils.C.target_info -> Z.t

sizeof t computes the size (in bytes) of a C type t

val sizeof_type : MopsaLib.typ -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> Z.t
val sizeof_type_in_host : MopsaLib.typ -> Z.t

Size (in bytes) of a type, as an expression. Handles variable-length ararys.

val remove_typedef : MopsaLib.typ -> MopsaLib.typ
val remove_qual : MopsaLib.typ -> MopsaLib.typ
val remove_typedef_qual : MopsaLib.typ -> MopsaLib.typ
val is_signed : MopsaLib.typ -> bool

is_signed t whether t is signed

val rangeof : MopsaLib.typ -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> Z.t * Z.t

range t computes the interval range of type t

val int_rangeof : MopsaLib.typ -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> int * int

range 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.expr

wrap_expr e (l,h) expression needed to bring back e in range (l,h)

val is_c_char_type : MopsaLib.typ -> bool
val is_c_string_type : MopsaLib.typ -> bool
val is_c_int_type : MopsaLib.typ -> bool

is_c_int_type t tests whether t is an integer type

val is_c_int_array_type : MopsaLib.typ -> bool
val is_c_signed_int_type : MopsaLib.typ -> bool
val is_c_bool_type : MopsaLib.typ -> bool
val is_c_float_type : MopsaLib.typ -> bool

is_c_int_type t tests whether t is a floating point type

val get_c_float_type : MopsaLib.typ -> c_float_type
val get_c_float_precision : MopsaLib.typ -> Universal.Lang.Ast.float_prec

Get the float precision from a C type

val is_c_bitfield : MopsaLib.typ -> bool
val is_c_num_type : MopsaLib.typ -> bool

is_c_int_type t tests whether t is a numeric type

val is_c_scalar_type : MopsaLib.typ -> bool

is_c_scalar_type t tests whether t is a scalar type

val is_c_pointer_type : MopsaLib.typ -> bool

is_c_pointer t tests whether t is a pointer

val is_c_void_type : MopsaLib.typ -> bool
val is_c_record_type : MopsaLib.typ -> bool
val is_c_struct_type : MopsaLib.typ -> bool
val is_c_union_type : MopsaLib.typ -> bool
val is_c_array_type : MopsaLib.typ -> bool
val is_c_function_type : MopsaLib.typ -> bool
val pointer_type : MopsaLib.typ -> MopsaLib.typ

is_scalartype t lifts t to a pointer to t

val under_pointer_type : MopsaLib.typ -> MopsaLib.typ
val under_array_type : MopsaLib.typ -> MopsaLib.typ
val under_type : MopsaLib.typ -> MopsaLib.typ
val void_to_char : MopsaLib.typ -> MopsaLib.typ
val get_array_constant_length : MopsaLib.typ -> Z.t
val align_byte : MopsaLib.typ -> int -> int
val is_c_type : MopsaLib.typ -> bool
val is_c_function_parameter : MopsaLib.var -> bool
val mk_c_member_access_by_name : MopsaLib.expr -> string -> Mopsa_utils.Core.Location.range -> MopsaLib.expr
val mk_c_arrow_access_by_name : MopsaLib.expr -> string -> Mopsa_utils.Core.Location.range -> MopsaLib.expr
val extract_multibyte_integer : string -> int -> MopsaLib.typ -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> Z.t
val mk_c_multibyte_integer : string -> int -> MopsaLib.typ -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> Mopsa_utils.Core.Location.range -> MopsaLib.expr
val mk_c_invalid_pointer : Mopsa_utils.Core.Location.range -> MopsaLib.expr
val void : MopsaLib.typ
val u8 : MopsaLib.typ
val s8 : MopsaLib.typ
val s16 : MopsaLib.typ
val u16 : MopsaLib.typ
val s32 : MopsaLib.typ
val u32 : MopsaLib.typ
val s64 : MopsaLib.typ
val u64 : MopsaLib.typ
val ul : MopsaLib.typ
val sl : MopsaLib.typ
val ull : MopsaLib.typ
val sll : MopsaLib.typ
val array_type : MopsaLib.typ -> Z.t -> MopsaLib.typ
val type_of_string : string -> MopsaLib.typ
val is_c_block_object_type : MopsaLib.typ -> bool
val to_c_block_object : MopsaLib.expr -> MopsaLib.expr
val of_c_block_object : MopsaLib.expr -> MopsaLib.expr
val mk_c_string : ?kind:c_character_kind -> string -> Mopsa_utils.Core.Location.range -> MopsaLib.expr
val mk_c_fun_typ : c_fundec -> MopsaLib.typ
val mk_c_null : ?esynthetic:bool -> Mopsa_utils.Core.Location.range -> MopsaLib.expr
val is_c_global_scope : c_var_scope -> bool
val find_c_record_field : int -> MopsaLib.typ -> c_record_field

Statement comparison *

val compare_c_var_init : c_var_init -> c_var_init -> int
val compare_c_fundec : c_fundec -> c_fundec -> int
val compare_c_var_scope : c_var_scope -> c_var_scope -> int
val compare_c_var_scope_update : c_scope_update -> c_scope_update -> int
val range_cond : MopsaLib.expr -> Z.t -> Z.t -> Mopsa_utils.Core.Location.range -> MopsaLib.expr
val remove_casts : MopsaLib.expr -> MopsaLib.expr
val c_expr_to_z : MopsaLib.expr -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> Z.t option

Simplify C constant expressions to constants

val is_c_expr_equals_z : MopsaLib.expr -> Z.t -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> bool
val is_c_constant : MopsaLib.expr -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> bool
val is_c_lval : MopsaLib.expr -> bool
val is_c_deref : MopsaLib.expr -> bool
val get_c_deref_type : MopsaLib.expr -> MopsaLib.typ
val is_c_variable_length_array_type : MopsaLib.typ -> bool

Check if v is declared as a variable length array

val is_c_no_length_array_type : MopsaLib.typ -> bool

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

Find the definition of a C function

val find_c_fundec_by_uid : int -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> c_fundec

Check if a pointer points to a nul-terminated array

Check if a pointer points to a nul-terminated wide char array

Check if a pointer points to a valid stream

Check if a pointer points to a valid file descriptor

Check if a pointer is valid

Randomize an entire array

Randomize a string

Randomize a substring

Randomize a wide substring

Set elements of an array with the same value c

Copy elements of an array

Exit if status is non-zero

Exit if status is non-zero

val var_scope : MopsaLib.var -> c_var_scope