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_common/C_common/Common/Alarms/index.html

Module Common.AlarmsSource

Alarms for C runtime errors

Utility print functions

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

Sourceval pp_const_or_interval : Stdlib.Format.formatter -> Universal.Numeric.Common.I.t Mopsa.Bot.with_bot -> unit

Print an interval depending on its cardinal

Sourceval pp_const_or_interval_not_eq : Stdlib.Format.formatter -> (Universal.Numeric.Common.I.B.t * Universal.Numeric.Common.I.B.t) Mopsa.Bot.with_bot -> unit

Print the not-member operator of an interval, depending on its cardinal

Sourceval pp_interval_plurial : Stdlib.Format.formatter -> (Universal.Numeric.Common.I.B.t * Universal.Numeric.Common.I.B.t) Mopsa.Bot.with_bot -> unit
Sourceval pp_interval_cardinal_plurial : Stdlib.Format.formatter -> (Universal.Numeric.Common.I.B.t * Universal.Numeric.Common.I.B.t) Mopsa.Bot.with_bot -> unit
Sourceval pp_base_verbose : Stdlib.Format.formatter -> C_common__.Base.base -> unit

Checks for invalid memory access

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

Sourcetype Mopsa.check +=
  1. | CHK_C_INVALID_MEMORY_ACCESS
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_null_deref of Mopsa.expr
    (*

    pointer

    *)
  2. | A_c_invalid_deref of Mopsa.expr
  3. | A_c_out_of_bound of C_common__.Base.base * Universal.Numeric.Common.int_itv * Universal.Numeric.Common.int_itv * Universal.Numeric.Common.int_itv
    (*

    accessed bytes

    *)
  4. | A_c_opaque_access of C_common__.Base.base * int * Universal.Numeric.Common.int_itv * Universal.Numeric.Common.int_itv
    (*

    accessed bytes

    *)
  5. | A_c_dangling_pointer_deref of Mopsa.expr * Mopsa.var * Mopsa.range
    (*

    return location

    *)
  6. | A_c_use_after_free of Mopsa.expr * Mopsa.range
    (*

    deallocation site

    *)
  7. | A_c_modify_read_only of Mopsa.expr * C_common__.Base.base
    (*

    pointed base

    *)
Sourceval raise_c_null_deref_alarm : ?bottom:bool -> Mopsa.expr -> ?range:Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_invalid_deref_alarm : ?bottom:bool -> Mopsa.expr -> ?range:Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_out_bound_alarm : ?bottom:bool -> C_common__.Base.base -> Ast.Expr.expr -> Ast.Expr.expr -> Mopsa.typ -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_opaque_access : ?bottom:bool -> C_common__.Base.base -> int -> Ast.Expr.expr -> Mopsa.typ -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_dangling_deref_alarm : ?bottom:bool -> Mopsa.expr -> Mopsa.var -> Mopsa.range -> ?range:Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_use_after_free_alarm : ?bottom:bool -> Mopsa.expr -> Mopsa.range -> ?range:Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_modify_read_only_alarm : ?bottom:bool -> Mopsa.expr -> C_common__.Base.base -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval safe_c_memory_access_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval unreachable_c_memory_access_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval raise_c_memory_access_warning : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Division by zero

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

Sourcetype Mopsa.check +=
  1. | CHK_C_DIVIDE_BY_ZERO
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_divide_by_zero of Mopsa.expr
    (*

    denominator

    *)
Sourceval raise_c_divide_by_zero_alarm : ?bottom:bool -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval safe_c_divide_by_zero_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval unreachable_c_divide_by_zero_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Integer overflow

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

Sourcetype Mopsa.check +=
  1. | CHK_C_INTEGER_OVERFLOW
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_integer_overflow of Mopsa.expr * Universal.Numeric.Common.int_itv * Mopsa.typ
    (*

    overflowed type

    *)
  2. | A_c_pointer_to_integer_overflow of Mopsa.expr * Mopsa.typ
    (*

    cast type

    *)
Sourceval raise_c_integer_overflow_alarm : ?warning:bool -> Mopsa.expr -> Ast.Expr.expr -> Mopsa.typ -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_pointer_to_integer_overflow_alarm : ?warning:bool -> Mopsa.expr -> Mopsa.typ -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval safe_c_integer_overflow_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval unreachable_c_integer_overflow_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Invalid shift

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

Sourcetype Mopsa.check +=
  1. | CHK_C_INVALID_SHIFT
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_invalid_shift of Mopsa.expr * Mopsa.expr * Universal.Numeric.Common.int_itv
    (*

    shift value

    *)
Sourceval raise_c_invalid_shift_alarm : ?bottom:bool -> Mopsa.expr -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval safe_c_shift_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval unreachable_c_shift_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Invalid pointer comparison

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

Sourcetype Mopsa.check +=
  1. | CHK_C_INVALID_POINTER_COMPARE
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_invalid_pointer_compare of Mopsa.expr * Mopsa.expr
    (*

    second pointer

    *)
Sourceval raise_c_invalid_pointer_compare : ?bottom:bool -> Mopsa.expr -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval safe_c_pointer_compare : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Invalid pointer subtraction

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

Sourcetype Mopsa.check +=
  1. | CHK_C_INVALID_POINTER_SUB
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_invalid_pointer_sub of Mopsa.expr * Mopsa.expr
    (*

    second pointer

    *)
Sourceval raise_c_invalid_pointer_sub : ?bottom:bool -> Mopsa.expr -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval safe_c_pointer_sub : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Double free

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

Sourcetype Mopsa.check +=
  1. | CHK_C_DOUBLE_FREE
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_double_free of Mopsa.expr * Mopsa.range
    (*

    deallocation site

    *)
Sourceval raise_c_double_free_alarm : ?bottom:bool -> Mopsa.expr -> Mopsa.range -> ?range:Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow

Insufficient variadic arguments

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

Sourcetype Mopsa.check +=
  1. | CHK_C_INSUFFICIENT_VARIADIC_ARGS
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_insufficient_variadic_args of Mopsa.var * Universal.Numeric.Common.int_itv * Universal.Numeric.Common.int_itv
    (*

    number of passed arguments

    *)
Sourceval raise_c_insufficient_variadic_args : ?bottom:bool -> Mopsa.var -> Ast.Expr.expr -> 'a list -> Mopsa_utils.Location.range -> ('b, 'c) Mopsa.man -> 'b Core.Flow.flow -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval safe_variadic_args_number : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Insufficient format arguments

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

Sourcetype Mopsa.check +=
  1. | CHK_C_INSUFFICIENT_FORMAT_ARGS
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_insufficient_format_args of int * int
    (*

    number of given arguments

    *)
Sourceval raise_c_insufficient_format_args_alarm : int -> int -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_insufficient_format_args_warning : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval safe_c_format_args_number : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Invalid type of format argument

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

Sourcetype Mopsa.check +=
  1. | CHK_C_INVALID_FORMAT_ARG_TYPE
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_invalid_format_arg_type of Mopsa.expr * Mopsa.typ
    (*

    expected type

    *)
Sourceval raise_c_invalid_format_arg_type_alarm : Mopsa.expr -> Mopsa.typ -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_invalid_format_arg_type_warning : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval safe_c_format_arg_type : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Float errors

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

Sourcetype Mopsa.check +=
  1. | CHK_C_INVALID_FLOAT_CLASS
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_invalid_float_class of Universal.Numeric.Common.float_itv * string
    (*

    expected class

    *)
Sourceval raise_c_invalid_float_class_alarm : ?bottom:bool -> Ast.Expr.expr -> string -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Core.Flow.flow -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourcetype Mopsa.check +=
  1. | CHK_C_FLOAT_INVALID_OPERATION
  2. | CHK_C_FLOAT_DIVISION_BY_ZERO
  3. | CHK_C_FLOAT_OVERFLOW

There are five IEEE 754 exceptions. We only singal include invalid operation, division by zero and overflow. We don't care about underflow (rounding to 0) and inexact (rounding).

Sourcetype Mopsa.alarm_kind +=
  1. | A_c_float_invalid_operation of Mopsa.expr * Universal.Numeric.Common.float_itv * Mopsa.typ
    (*

    destination type

    *)
  2. | A_c_float_division_by_zero of Mopsa.expr * Universal.Numeric.Common.float_itv
    (*

    denominator interval

    *)
  3. | A_c_float_overflow of Mopsa.expr * Universal.Numeric.Common.float_itv * Mopsa.typ
    (*

    type

    *)
Sourceval raise_c_float_invalid_operation_alarm : ?bottom:bool -> ?warning:bool -> Mopsa.expr -> Universal.Numeric.Common.float_itv -> Mopsa.typ -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_float_division_by_zero_alarm : ?bottom:bool -> ?warning:bool -> Mopsa.expr -> Universal.Numeric.Common.float_itv -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval raise_c_float_overflow_alarm : ?bottom:bool -> ?warning:bool -> Mopsa.expr -> Universal.Numeric.Common.float_itv -> Mopsa.typ -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval safe_c_float_invalid_operation_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval safe_c_float_division_by_zero_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval safe_c_float_overflow_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Unfreed/Unreachable memory

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

Sourcetype Mopsa.check +=
  1. | CHK_C_UNREACHABLE_MEMORY
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_unreachable_memory of Mopsa.addr
Sourceval raise_c_unreachable_memory : Mopsa.addr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow

Invalid array size

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

Sourcetype Mopsa.check +=
  1. | CHK_C_NEGATIVE_ARRAY_SIZE
Sourcetype Mopsa.alarm_kind +=
  1. | A_c_negative_array_size of Mopsa.expr
Sourceval raise_c_negative_array_size_alarm : ?bottom:bool -> Mopsa.expr -> Mopsa_utils.Location.range -> ('a, 'b) Mopsa.man -> 'a Mopsa.Flow.flow -> 'a Mopsa.Flow.flow
Sourceval safe_c_negative_array_size_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
Sourceval unreachable_c_negative_array_size_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow