package mopsa

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

Module Common.Alarms

Alarms for C runtime errors

Utility print functions

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

Print an interval depending on its cardinal

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

val pp_base_verbose : Format.formatter -> Base.base -> unit

Checks for invalid memory access

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

type MopsaLib.check +=
  1. | CHK_C_INVALID_MEMORY_ACCESS
type MopsaLib.alarm_kind +=
  1. | A_c_null_deref of MopsaLib.expr
    (*

    pointer

    *)
  2. | A_c_invalid_deref of MopsaLib.expr
  3. | A_c_out_of_bound of 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 Base.base * int * Universal.Numeric.Common.int_itv * Universal.Numeric.Common.int_itv
    (*

    accessed bytes

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

    return location

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

    deallocation site

    *)
  7. | A_c_modify_read_only of MopsaLib.expr * Base.base
    (*

    pointed base

    *)
val raise_c_null_deref_alarm : ?bottom:bool -> MopsaLib.expr -> ?range:Mopsa_utils.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow
val raise_c_invalid_deref_alarm : ?bottom:bool -> MopsaLib.expr -> ?range:Mopsa_utils.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow
val raise_c_use_after_free_alarm : ?bottom:bool -> MopsaLib.expr -> MopsaLib.range -> ?range:Mopsa_utils.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow
val raise_c_modify_read_only_alarm : ?bottom:bool -> MopsaLib.expr -> Base.base -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow

Division by zero

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

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

    denominator

    *)
val raise_c_divide_by_zero_alarm : ?bottom:bool -> MopsaLib.expr -> Mopsa_utils.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow

Integer overflow

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

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

    overflowed type

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

    cast type

    *)
val raise_c_pointer_to_integer_overflow_alarm : ?warning:bool -> MopsaLib.expr -> MopsaLib.typ -> Mopsa_utils.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow

Invalid shift

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

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

    shift value

    *)

Invalid pointer comparison

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

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

    second pointer

    *)

Invalid pointer subtraction

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

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

    second pointer

    *)

Double free

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

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

    deallocation site

    *)

Insufficient variadic arguments

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

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

    number of passed arguments

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

Insufficient format arguments

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

type MopsaLib.check +=
  1. | CHK_C_INSUFFICIENT_FORMAT_ARGS
type MopsaLib.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.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow
val raise_c_insufficient_format_args_warning : Mopsa_utils.Core.Location.range -> 'a -> 'b Mopsa_analyzer.MopsaLib.Flow.flow -> 'b Mopsa_analyzer.MopsaLib.Flow.flow

Invalid type of format argument

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

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

    expected type

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

Float errors

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

type MopsaLib.check +=
  1. | CHK_C_INVALID_FLOAT_CLASS
type MopsaLib.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 -> Framework.Core.Ast.Expr.expr -> string -> Mopsa_utils.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Core.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow
type MopsaLib.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 MopsaLib.alarm_kind +=
  1. | A_c_float_invalid_operation of MopsaLib.expr * Universal.Numeric.Common.float_itv * MopsaLib.typ
    (*

    destination type

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

    denominator interval

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

    type

    *)
val raise_c_float_invalid_operation_alarm : ?bottom:bool -> ?warning:bool -> MopsaLib.expr -> Universal.Numeric.Common.float_itv -> MopsaLib.typ -> Mopsa_utils.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow
val raise_c_float_division_by_zero_alarm : ?bottom:bool -> ?warning:bool -> MopsaLib.expr -> Universal.Numeric.Common.float_itv -> Mopsa_utils.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow

Unfreed/Unreachable memory

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

type MopsaLib.check +=
  1. | CHK_C_UNREACHABLE_MEMORY
type MopsaLib.alarm_kind +=
  1. | A_c_unreachable_memory of MopsaLib.addr

Invalid array size

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

type MopsaLib.check +=
  1. | CHK_C_NEGATIVE_ARRAY_SIZE
type MopsaLib.alarm_kind +=
  1. | A_c_negative_array_size of MopsaLib.expr
val raise_c_negative_array_size_alarm : ?bottom:bool -> MopsaLib.expr -> Mopsa_utils.Core.Location.range -> ('a, 'b) MopsaLib.man -> 'a Mopsa_analyzer.MopsaLib.Flow.flow -> 'a Mopsa_analyzer.MopsaLib.Flow.flow
val unreachable_c_negative_array_size_check : Mopsa_utils.Core.Location.range -> 'a -> 'b Mopsa_analyzer.MopsaLib.Flow.flow -> 'b Mopsa_analyzer.MopsaLib.Flow.flow

Incorrect number of arguments

type MopsaLib.check +=
  1. | CHK_C_INCORRECT_NUMBER_OF_ARGUMENTS
type MopsaLib.alarm_kind +=
  1. | A_c_incorrect_number_of_arguments of Lang.Ast.c_fundec * MopsaLib.expr list
    (*

    arguments

    *)
val safe_c_incorrect_number_of_arguments_check : Mopsa_utils.Core.Location.range -> 'a -> 'b Mopsa_analyzer.MopsaLib.Flow.flow -> 'b Mopsa_analyzer.MopsaLib.Flow.flow