package mopsa

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

Install 

dune-project
 Dependency

gitlab.com 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.0.tar.gz
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4

doc/c_lang/C_lang/Lang/Ast/index.html

Module Lang.AstSource

AST of the C language.

Types

Sourcetype 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 : Mopsa.typ;
    (*

    declaration

    *)
  4. c_typedef_range : Mopsa.Location.range;
    (*

    declaration location

    *)
}

Type definition.

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

    Whether a record is struct or union.

    *)
Sourceand 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.Location.range;
    (*

    declaration location

    *)
}

Struct or union type.

Sourceand 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 : Mopsa.typ;
  6. c_field_range : Mopsa.Location.range;
    (*

    declaration location

    *)
  7. c_field_index : int;
}

Struct or union field.

Sourceand 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.Location.range;
    (*

    declaration location

    *)
}

Enumerated type.

Sourceand 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 : Mopsa.range;
}

A possible value in an enumerated type.

Sourceand 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.

    *)
Sourceand c_float_type =
  1. | C_float
  2. | C_double
  3. | C_long_double
  4. | C_float128
    (*

    Floating-point types.

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

    Cases of arrays length.

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

Type qualifiers.

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

Function type.

Sourcetype Mopsa.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 Mopsa.typ
    (*

    Scalar types.

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

    Arrays.

    *)
  7. | T_c_bitfield of Mopsa.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 * Mopsa.typ
    (*

    Qualified type.

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

    Type of block objects.

    *)

Function descriptor

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

Sourcetype 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 : Mopsa.typ;
    (*

    type of returned value

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

    function parameters

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

    function body

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

    static variables declared in the function

    *)
  9. mutable c_func_local_vars : Mopsa.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 : Mopsa.range;
    (*

    location range of the declaration

    *)
  12. mutable c_func_name_range : Mopsa.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

Sourcetype 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

    *)
Sourceval pp_scope : Stdlib.Format.formatter -> c_var_scope -> unit
Sourcetype c_var_init =
  1. | C_init_expr of Mopsa.expr
  2. | C_init_list of c_var_init list * c_var_init option
    (*

    filler

    *)
  3. | C_init_implicit of Mopsa.typ

Variable initialization.

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

    life-time scope of the variable

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

    declaration range

    *)
  3. cvar_uid : int;
  4. cvar_orig_name : string;
  5. cvar_uniq_name : string;
}
Sourcetype Mopsa.var_kind +=
  1. | V_cvar of cvar
    (*

    C variable

    *)

C expressions

Sourcetype Mopsa.operator +=
  1. | O_c_and
  2. | O_c_or
Sourcetype c_inc_location =
  1. | PRE
  2. | POST
    (*

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

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

    Whether an incrementation is ++ or --

    *)
Sourcetype 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
Sourcetype Mopsa.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

    *)
Sourcetype Mopsa.expr_kind +=
  1. | E_c_conditional of Mopsa.expr * Mopsa.expr * Mopsa.expr
    (*

    else

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

    index

    *)
  3. | E_c_member_access of Mopsa.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 * Mopsa.expr list
  7. | E_c_arrow_access of Mopsa.expr * int * string
    (*

    field

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

    rvalue

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

    type of the result, before converting back to lvalue type

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

    , operator

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

    & operator (address of lvalue)

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

    * operator (pointer dereference)

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

    explicitness

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

    predefined identifier

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

    __builtin_va_arg

    *)
  18. | E_c_atomic of int * Mopsa.expr * Mopsa.expr
  19. | E_c_block_object of Mopsa.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

Sourcetype c_scope_update = {
  1. c_scope_var_added : Mopsa.var list;
  2. c_scope_var_removed : Mopsa.var list;
}

Scope update information for jump statements

Statements

Sourcetype Mopsa.stmt_kind +=
  1. | S_c_goto_stab of Mopsa.stmt
    (*

    stabilization point for goto statement

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

    declaration of a variable

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

    condition

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

    body

    *)
  5. | S_c_return of Mopsa.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 Mopsa.expr * Mopsa.stmt
    (*

    switch statement.

    *)
  10. | S_c_label of string
    (*

    statement label.

    *)
  11. | S_c_switch_case of Mopsa.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

    *)
Sourcetype c_program = {
  1. c_globals : (Mopsa.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

    *)
}
Sourcetype Mopsa.prog_kind +=
  1. | C_program of c_program
module CProgramKey : sig ... end
Sourceval c_program_ctx : ('a, c_program) Core__Context.ctx_key

Flow-insensitive context to keep the analyzed C program

Sourceval set_c_program : c_program -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow

Set the C program in the flow

Sourceval get_c_program : 'a Mopsa.Flow.flow -> c_program

Get the C program from the flow

Conversion to/from Clang parser types

Target information

module TargetCtx : sig ... end
Sourceval remove_c_target_info : 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow

Sizes and alignments

Sourceval sizeof_type_in_target : Mopsa.typ -> Mopsa_c_parser.C_utils.C.target_info -> Z.t

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

Sourceval sizeof_type : Mopsa.typ -> 'a Mopsa.Flow.flow -> Z.t
Sourceval sizeof_type_in_host : Mopsa.typ -> Z.t

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

Sourceval remove_typedef : Mopsa.typ -> Mopsa.typ
Sourceval remove_qual : Mopsa.typ -> Mopsa.typ
Sourceval remove_typedef_qual : Mopsa.typ -> Mopsa.typ
Sourceval is_signed : Mopsa.typ -> bool

is_signed t whether t is signed

Sourceval rangeof : Mopsa.typ -> 'a Mopsa.Flow.flow -> Z.t * Z.t

range t computes the interval range of type t

Sourceval int_rangeof : Mopsa.typ -> 'a Mopsa.Flow.flow -> int * int

range t computes the interval range of type t as integers

Sourceval wrap_expr : Mopsa.expr -> (Z.t * Z.t) -> Mopsa_utils.Location.range -> Mopsa.expr

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

Sourceval is_c_char_type : Mopsa.typ -> bool
Sourceval is_c_string_type : Mopsa.typ -> bool
Sourceval is_c_int_type : Mopsa.typ -> bool

is_c_int_type t tests whether t is an integer type

Sourceval is_c_int_array_type : Mopsa.typ -> bool
Sourceval is_c_signed_int_type : Mopsa.typ -> bool
Sourceval is_c_bool_type : Mopsa.typ -> bool
Sourceval is_c_float_type : Mopsa.typ -> bool

is_c_int_type t tests whether t is a floating point type

Sourceval get_c_float_type : Mopsa.typ -> c_float_type
Sourceval get_c_float_precision : Mopsa.typ -> Universal.Ast.float_prec

Get the float precision from a C type

Sourceval is_c_bitfield : Mopsa.typ -> bool
Sourceval is_c_num_type : Mopsa.typ -> bool

is_c_int_type t tests whether t is a numeric type

Sourceval is_c_scalar_type : Mopsa.typ -> bool

is_c_scalar_type t tests whether t is a scalar type

Sourceval is_c_pointer_type : Mopsa.typ -> bool

is_c_pointer t tests whether t is a pointer

Sourceval is_c_void_type : Mopsa.typ -> bool
Sourceval is_c_record_type : Mopsa.typ -> bool
Sourceval is_c_struct_type : Mopsa.typ -> bool
Sourceval is_c_union_type : Mopsa.typ -> bool
Sourceval is_c_array_type : Mopsa.typ -> bool
Sourceval is_c_function_type : Mopsa.typ -> bool
Sourceval pointer_type : Mopsa.typ -> Mopsa.typ

is_scalartype t lifts t to a pointer to t

Sourceval under_pointer_type : Mopsa.typ -> Mopsa.typ
Sourceval under_array_type : Mopsa.typ -> Mopsa.typ
Sourceval under_type : Mopsa.typ -> Mopsa.typ
Sourceval void_to_char : Mopsa.typ -> Mopsa.typ
Sourceval get_array_constant_length : Mopsa.typ -> Z.t
Sourceval align_byte : Mopsa.typ -> int -> int
Sourceval is_c_type : Mopsa.typ -> bool
Sourceval is_c_function_parameter : Mopsa.var -> bool
Sourceval mk_c_member_access_by_name : Mopsa.expr -> string -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_c_arrow_access_by_name : Mopsa.expr -> string -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_c_character : char -> Mopsa_utils.Location.range -> Mopsa.typ -> Mopsa.expr
Sourceval extract_multibyte_integer : string -> int -> Mopsa.typ -> 'a Mopsa.Flow.flow -> Z.t
Sourceval mk_c_multibyte_integer : string -> int -> Mopsa.typ -> 'a Mopsa.Flow.flow -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_c_invalid_pointer : Mopsa_utils.Location.range -> Mopsa.expr
Sourceval void : Mopsa.typ
Sourceval s16 : Mopsa.typ
Sourceval u16 : Mopsa.typ
Sourceval s32 : Mopsa.typ
Sourceval u32 : Mopsa.typ
Sourceval s64 : Mopsa.typ
Sourceval u64 : Mopsa.typ
Sourceval ull : Mopsa.typ
Sourceval sll : Mopsa.typ
Sourceval array_type : Mopsa.typ -> Z.t -> Mopsa.typ
Sourceval size_type : 'a Mopsa.Flow.flow -> Mopsa.typ
Sourceval type_of_string : string -> Mopsa.typ
Sourceval is_c_block_object_type : Mopsa.typ -> bool
Sourceval to_c_block_object : Mopsa.expr -> Mopsa.expr
Sourceval of_c_block_object : Mopsa.expr -> Mopsa.expr
Sourceval mk_c_string : ?kind:c_character_kind -> string -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval mk_c_fun_typ : c_fundec -> Mopsa.typ
Sourceval mk_c_builtin_call : string -> Mopsa.expr list -> Ast.Typ.typ -> Mopsa_utils.Location.range -> Mopsa.expr
Sourceval is_c_global_scope : c_var_scope -> bool

Statement comparison *

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

Simplify C constant expressions to constants

Sourceval is_c_expr_equals_z : Mopsa.expr -> Z.t -> 'a Mopsa.Flow.flow -> bool
Sourceval is_c_constant : Mopsa.expr -> 'a Mopsa.Flow.flow -> bool
Sourceval is_c_lval : Mopsa.expr -> bool
Sourceval is_c_deref : Mopsa.expr -> bool
Sourceval get_c_deref_type : Mopsa.expr -> Mopsa.typ
Sourceval is_c_variable_length_array_type : Mopsa.typ -> bool

Check if v is declared as a variable length array

Sourceval is_c_no_length_array_type : Mopsa.typ -> bool

Check if v is declared as an array without length (as for many auxiliary variables)

Sourceval find_c_fundec_by_name : string -> 'a Mopsa.Flow.flow -> c_fundec

Find the definition of a C function

Sourceval find_c_fundec_by_uid : int -> 'a Mopsa.Flow.flow -> c_fundec
Sourceval assert_valid_string : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Check if a pointer points to a nul-terminated array

Sourceval assert_valid_wide_string : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

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

Sourceval assert_valid_stream : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Check if a pointer points to a valid stream

Sourceval assert_valid_file_descriptor : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Check if a pointer points to a valid file descriptor

Sourceval assert_valid_ptr : Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

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

Sourceval error_error_at_line : Mopsa.expr -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Post.post

Exit if status is non-zero

Sourceval vasprintf_stub : bool -> Mopsa.expr -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Core.Eval.eval

Stack variables

Sourcetype Mopsa.var_kind +=
  1. | V_c_stack_var of Mopsa.callstack * Mopsa.var

This vkind is used to attach the callstack to local variables

Sourceval mk_stack_var : Mopsa.callstack -> Mopsa.var -> Mopsa.var

Create a stack variable

Sourceval var_scope : Mopsa.var -> c_var_scope