Module `Common.Alarms`

Alarms for C runtime errors

Utility print functions

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

val pp_const_or_interval : 
  Format.formatter ->
  Mopsa_analyzer.MopsaLib.ItvUtils.IntItv.t Mopsa_utils.Core.Bot.with_bot ->
  unit

Print an interval depending on its cardinal

val pp_const_or_interval_not_eq : 
  Format.formatter ->
  (Mopsa_analyzer.MopsaLib.ItvUtils.IntItv.B.t
   * Mopsa_analyzer.MopsaLib.ItvUtils.IntItv.B.t)
    Mopsa_utils.Core.Bot.with_bot ->
  unit

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

val pp_interval_plurial : 
  Format.formatter ->
  (Mopsa_analyzer.MopsaLib.ItvUtils.IntItv.B.t
   * Mopsa_analyzer.MopsaLib.ItvUtils.IntItv.B.t)
    Mopsa_utils.Core.Bot.with_bot ->
  unit

val pp_interval_cardinal_plurial : 
  Format.formatter ->
  (Mopsa_analyzer.MopsaLib.ItvUtils.IntItv.B.t
   * Mopsa_analyzer.MopsaLib.ItvUtils.IntItv.B.t)
    Mopsa_utils.Core.Bot.with_bot ->
  unit

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

Checks for invalid memory access

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

type MopsaLib.check +=

| CHK_C_INVALID_MEMORY_ACCESS

type MopsaLib.alarm_kind +=

| A_c_null_deref of MopsaLib.expr
(*
pointer
*)
| A_c_invalid_deref of MopsaLib.expr
| 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
*)
| A_c_opaque_access of Base.base * int * Universal.Numeric.Common.int_itv * Universal.Numeric.Common.int_itv
(*
accessed bytes
*)
| A_c_dangling_pointer_deref of MopsaLib.expr * MopsaLib.var * MopsaLib.range
(*
return location
*)
| A_c_use_after_free of MopsaLib.expr * MopsaLib.range
(*
deallocation site
*)
| 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_out_bound_alarm : 
  ?bottom:bool ->
  Base.base ->
  Framework.Core.Ast.Expr.expr ->
  Framework.Core.Ast.Expr.expr ->
  MopsaLib.typ ->
  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

val raise_c_opaque_access : 
  ?bottom:bool ->
  Base.base ->
  int ->
  Framework.Core.Ast.Expr.expr ->
  MopsaLib.typ ->
  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

val raise_c_dangling_deref_alarm : 
  ?bottom:bool ->
  MopsaLib.expr ->
  MopsaLib.var ->
  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_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

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

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

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

Division by zero

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

type MopsaLib.check +=

| CHK_C_DIVIDE_BY_ZERO

type MopsaLib.alarm_kind +=

| 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

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

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

Integer overflow

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

type MopsaLib.check +=

| CHK_C_INTEGER_OVERFLOW

type MopsaLib.alarm_kind +=

| A_c_integer_overflow of MopsaLib.expr * Universal.Numeric.Common.int_itv * MopsaLib.typ
(*
overflowed type
*)
| A_c_pointer_to_integer_overflow of MopsaLib.expr * MopsaLib.typ
(*
cast type
*)

val raise_c_integer_overflow_alarm : 
  ?warning:bool ->
  MopsaLib.expr ->
  Framework.Core.Ast.Expr.expr ->
  MopsaLib.typ ->
  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

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

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

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

Invalid shift

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

type MopsaLib.check +=

| CHK_C_INVALID_SHIFT

type MopsaLib.alarm_kind +=

| A_c_invalid_shift of MopsaLib.expr * MopsaLib.expr * Universal.Numeric.Common.int_itv
(*
shift value
*)

val raise_c_invalid_shift_alarm : 
  ?bottom:bool ->
  MopsaLib.expr ->
  MopsaLib.expr ->
  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

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

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

Invalid pointer comparison

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

type MopsaLib.check +=

| CHK_C_INVALID_POINTER_COMPARE

type MopsaLib.alarm_kind +=

| A_c_invalid_pointer_compare of MopsaLib.expr * MopsaLib.expr
(*
second pointer
*)

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

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

Invalid pointer subtraction

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

type MopsaLib.check +=

| CHK_C_INVALID_POINTER_SUB

type MopsaLib.alarm_kind +=

| A_c_invalid_pointer_sub of MopsaLib.expr * MopsaLib.expr
(*
second pointer
*)

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

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

Double free

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

type MopsaLib.check +=

| CHK_C_DOUBLE_FREE

type MopsaLib.alarm_kind +=

| A_c_double_free of MopsaLib.expr * MopsaLib.range
(*
deallocation site
*)

val raise_c_double_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

Insufficient variadic arguments

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

type MopsaLib.check +=

| CHK_C_INSUFFICIENT_VARIADIC_ARGS

type MopsaLib.alarm_kind +=

| 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

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

Insufficient format arguments

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

type MopsaLib.check +=

| CHK_C_INSUFFICIENT_FORMAT_ARGS

type MopsaLib.alarm_kind +=

| 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

val safe_c_format_args_number : 
  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 +=

| CHK_C_INVALID_FORMAT_ARG_TYPE

type MopsaLib.alarm_kind +=

| 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

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

Float errors

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

type MopsaLib.check +=

| CHK_C_INVALID_FLOAT_CLASS

type MopsaLib.alarm_kind +=

| 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 +=

| CHK_C_FLOAT_INVALID_OPERATION
| CHK_C_FLOAT_DIVISION_BY_ZERO
| 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 +=

| A_c_float_invalid_operation of MopsaLib.expr * Universal.Numeric.Common.float_itv * MopsaLib.typ
(*
destination type
*)
| A_c_float_division_by_zero of MopsaLib.expr * Universal.Numeric.Common.float_itv
(*
denominator interval
*)
| 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

val raise_c_float_overflow_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 safe_c_float_invalid_operation_check : 
  Mopsa_utils.Core.Location.range ->
  'a ->
  'b Mopsa_analyzer.MopsaLib.Flow.flow ->
  'b Mopsa_analyzer.MopsaLib.Flow.flow

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

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

Unfreed/Unreachable memory

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

type MopsaLib.check +=

| CHK_C_UNREACHABLE_MEMORY

type MopsaLib.alarm_kind +=

| A_c_unreachable_memory of MopsaLib.addr

val raise_c_unreachable_memory : 
  MopsaLib.addr ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow

Invalid array size

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

type MopsaLib.check +=

| CHK_C_NEGATIVE_ARRAY_SIZE

type MopsaLib.alarm_kind +=

| 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 safe_c_negative_array_size_check : 
  Mopsa_utils.Core.Location.range ->
  'a ->
  'b Mopsa_analyzer.MopsaLib.Flow.flow ->
  'b 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 +=

| CHK_C_INCORRECT_NUMBER_OF_ARGUMENTS

type MopsaLib.alarm_kind +=

| A_c_incorrect_number_of_arguments of Lang.Ast.c_fundec * MopsaLib.expr list
(*
arguments
*)

val raise_c_incorrect_number_of_arguments_alarm : 
  Lang.Ast.c_fundec ->
  MopsaLib.expr list ->
  Mopsa_utils.Core.Location.range ->
  ('a, 'b) MopsaLib.man ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow ->
  'a Mopsa_analyzer.MopsaLib.Flow.flow

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

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/C/Common/Alarms/index.html

Module `Common.Alarms`

Utility print functions

Checks for invalid memory access

Division by zero

Integer overflow

Invalid shift

Invalid pointer comparison

Invalid pointer subtraction

Double free

Insufficient variadic arguments

Insufficient format arguments

Invalid type of format argument

Float errors

Unfreed/Unreachable memory

Invalid array size

Incorrect number of arguments

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_analyzer/Mopsa_analyzer/Languages/C/Common/Alarms/index.html

Module Common.Alarms

Utility print functions

Checks for invalid memory access

Division by zero

Integer overflow

Invalid shift

Invalid pointer comparison

Invalid pointer subtraction

Double free

Insufficient variadic arguments

Insufficient format arguments

Invalid type of format argument

Float errors

Unfreed/Unreachable memory

Invalid array size

Incorrect number of arguments

dune-project
Dependency

Module `Common.Alarms`