package mopsa

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

Module Machine_numbers.Domain

Domain identification

=====================

include sig ... end
val id : unit Mopsa_analyzer__Framework__Core__Id.id
val name : string
val debug : ('a, Format.formatter, unit, unit) format4 -> 'a
val universal : MopsaLib.route
val checks : MopsaLib.check list
val opt_signed_arithmetic_overflow_wraparound : bool ref

====================

val opt_signed_arithmetic_overflow : bool ref
val opt_unsigned_arithmetic_overflow : bool ref
val opt_signed_implicit_cast_overflow : bool ref
val opt_unsigned_implicit_cast_overflow : bool ref
val opt_explicit_cast_overflow : bool ref
val opt_float_invalid_operation : bool ref
val opt_float_division_by_zero : bool ref
val opt_float_overflow : bool ref
val opt_mnum_rela_query : bool ref

Numeric variables

=================

type MopsaLib.var_kind +=
  1. | V_c_num of MopsaLib.var

Kind of mathematical numeric variables encoding the value of C numeric variables (integers and floats)

val to_num_type : MopsaLib.typ -> MopsaLib.typ
val mk_num_var : MopsaLib.var -> MopsaLib.var
val mk_num_var_expr : MopsaLib.expr -> MopsaLib.expr

Utility functions

=================

val range_leq : (Z.t * Z.t) -> (Z.t * Z.t) -> bool
val wrap_z : Z.t -> (Z.t * Z.t) -> Z.t
val is_c_overflow_op : MopsaLib.operator -> bool
val is_c_div_op : MopsaLib.operator -> bool
val is_c_shift_op : MopsaLib.operator -> bool
val is_c_float_op : MopsaLib.operator -> bool

Rebuild a C expression from its parts

Build a numeric expression from a C expression

check_int_overflow cexp nexp ... checks whether the C expression cexp produces an integer overflow and transforms its numeric evaluation nexp accordingly

Check that a division is not performed on a null denominator

Check that bit-shifts are safe. Two conditions are verified: (i) the shift position is positive, and (ii) this position does not exceed the size of the shifted value

check_float_valid cexp nexp ... checks whether the C expression cexp produces an infinity or NaN result.

val check_float_division : MopsaLib.expr -> ('a, 'b) MopsaLib.man -> 'a Core.Flow.flow -> ('a, Framework.Core.Ast.Expr.expr) Core.Cases.cases

Check that a float division is not performed on a null denominator. Also checks for invalid operations and overflows.

Transfer functions

==================

val exec : MopsaLib.stmt -> ('a, 'b) MopsaLib.man -> 'a Core.Flow.flow -> ('a, unit) Mopsa_analyzer.MopsaLib.Cases.cases option
val ask : 'a -> 'b -> 'c -> 'd option
val init : 'a -> 'b -> 'c -> 'd option

Pretty printer

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

val print_expr : ('a, 'b) MopsaLib.man -> 'a Core.Flow.flow -> Framework.Core.Print.printer -> MopsaLib.expr -> unit