package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type

Alarms for C runtime errors

Utility print functions

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

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

Print an interval depending on its cardinal

val 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

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

Checks for invalid memory access

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

type Mopsa.check +=
  1. | CHK_C_INVALID_MEMORY_ACCESS
type 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

    *)
val 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
val 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
val 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
val 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
val 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
val 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
val 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
val safe_c_memory_access_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
val unreachable_c_memory_access_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
val raise_c_memory_access_warning : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Division by zero

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

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

    denominator

    *)
val 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
val safe_c_divide_by_zero_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
val unreachable_c_divide_by_zero_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Integer overflow

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

type Mopsa.check +=
  1. | CHK_C_INTEGER_OVERFLOW
type 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

    *)
val 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
val 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
val safe_c_integer_overflow_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
val unreachable_c_integer_overflow_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Invalid shift

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

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

    shift value

    *)
val 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
val safe_c_shift_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
val unreachable_c_shift_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Invalid pointer comparison

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

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

    second pointer

    *)
val 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
val safe_c_pointer_compare : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Invalid pointer subtraction

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

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

    second pointer

    *)
val 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
val safe_c_pointer_sub : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Double free

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

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

    deallocation site

    *)
val 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

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

type Mopsa.check +=
  1. | CHK_C_INSUFFICIENT_VARIADIC_ARGS
type 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

    *)
val 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
val safe_variadic_args_number : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Insufficient format arguments

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

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

    number of given arguments

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

Invalid type of format argument

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

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

    expected type

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

Float errors

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

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

    expected class

    *)
val 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
type 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).

type 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

    *)
val 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
val 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
val 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
val safe_c_float_invalid_operation_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
val safe_c_float_division_by_zero_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
val safe_c_float_overflow_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow

Unfreed/Unreachable memory

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

type Mopsa.check +=
  1. | CHK_C_UNREACHABLE_MEMORY
type Mopsa.alarm_kind +=
  1. | A_c_unreachable_memory of Mopsa.addr
val 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

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

type Mopsa.check +=
  1. | CHK_C_NEGATIVE_ARRAY_SIZE
type Mopsa.alarm_kind +=
  1. | A_c_negative_array_size of Mopsa.expr
val 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
val safe_c_negative_array_size_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
val unreachable_c_negative_array_size_check : Mopsa_utils.Location.range -> 'a -> 'b Mopsa.Flow.flow -> 'b Mopsa.Flow.flow
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct