(* * Copyright (c) 2002 by Laboratoire Spécification et Vérification (LSV), * CNRS UMR 8643 & ENS Cachan. * Written by Jean Goubault-Larrecq. Not derived from licensed software. * * Permission is granted to anyone to use this software for any * purpose on any computer system, and to redistribute it freely, * subject to the following restrictions: * * 1. Neither the author nor its employer is responsible for the consequences of use of * this software, no matter how awful, even if they arise * from defects in it. * * 2. The origin of this software must not be misrepresented, either * by explicit claim or by omission. * * 3. Altered versions must be plainly marked as such, and must not * be misrepresented as being the original software. * * 4. This software is restricted to non-commercial use only. Commercial * use is subject to a specific license, obtainable from LSV. *) open Intervalle (* Intervalles d'entiers. Pour chaque type entier (int, short, char, long et leurs versions unsigned), on represente le domaine de variation des entiers de ce type comme un intervalle. Les bornes it_min, it_max des entiers de chaque type qtyp sont donnees par Arith.int_type_info qtyp, qui retourne un record {it_min=...; it_max=...; it_range=...; it_signed=...; it_nbits=...} [de type Arith.int_type]; it_nbits est le nombre de bits dans le type, it_signed est vrai s'il s'agit d'un type signe, faux sinon, it_range est le nombre d'entiers dans le domaine. *) val itv_int_empty : itv (* le bottom des intervalles. *) val itv_int_full : Arith.int_type -> itv (* l'intervalle maximal [it_min, it_max] pour le int_type donne en entree. *) val itv_int_top : Cparse.q_ctype -> itv (* l'intervalle maximal [it_min, it_max] correspondant au type C en entree. *) val itv_int_widen : Arith.int_type -> itv -> itv -> itv (* l'elargissement, parametre par l'int_type du type donne. L'union est deja definie dans intervalle.ml. *) val itv_int_cst : Cparse.constant_val -> itv (* Convertit une constante entiere en intervalle. *) val itv_int_add : Arith.int_type -> itv -> itv -> itv (* L'addition, parametree par l'int_type du type des arguments et du resultat. *) val itv_int_minus : Arith.int_type -> itv -> itv (* L'oppose, parametre par l'int_type du type des arguments et du resultat. *) val itv_int_sub : Arith.int_type -> itv -> itv -> itv (* La soustraction, parametree par l'int_type du type des arguments et du resultat. *) val itv_int_mul : Arith.int_type -> itv -> itv -> itv (* La multiplication, parametree par l'int_type du type des arguments et du resultat. *) val itv_int_div : Arith.int_type -> itv -> itv -> itv * bool (* La division entiere, parametree par l'int_type du type des arguments et du resultat. *) val itv_int_mod : Arith.int_type -> itv -> itv -> itv * bool (* Le reste, parametre par l'int_type du type des arguments et du resultat. *) val itv_int_convert : Arith.int_type -> itv -> itv (* itv_int_convert it itv effectue la conversion des entiers dans itv en des entiers d'int_type it. Par exemple, si on ecrit en C: (short)n, ou n est de type unsigned long, alors itv sera un intervalle inclus dans [Arith.type_unsigned_long.it_min, Arith.type_unsigned_long.it_max], et la conversion doit aboutir a un intervalle de short, donc inclus dans [Arith.type_short.it_min, Arith.type_short.it_max]. *) val itv_int_convert_float : Arith.int_type -> itv * bool -> itv (* itv_int_convert_float it fitv convertit un intervalle flottant (cf. itv_float.mli) fitv en un entier d'int_type it. Attention, on supposera que les NaN peuvent se convertir en n'importe quel entier. *) val itv_int_le : Arith.int_type -> itv -> itv -> itv (* La relation <=; retourne un intervalle d'entiers possibles (les tests C retournent 1 si vrai, 0 si faux). Le premier argument est l'int_type des deux intervalles d'entiers a comparer. *) val itv_int_lt : Arith.int_type -> itv -> itv -> itv (* La relation <; retourne un intervalle d'entiers possibles (les tests C retournent 1 si vrai, 0 si faux). Le premier argument est l'int_type des deux intervalles d'entiers a comparer. *) val itv_int_eq : Arith.int_type -> itv -> itv -> itv (* La relation =; retourne un intervalle d'entiers possibles (les tests C retournent 1 si vrai, 0 si faux). Le premier argument est l'int_type des deux intervalles d'entiers a comparer. *) val itv_int_test_true : itv -> bool (* itv_int_test_true itv est vrai si et seulement s'il est possible qu'itv contienne un booleen vrai (entier non nul). *) val itv_int_test_false : itv -> bool (* itv_int_test_false itv est vrai si et seulement s'il est possible qu'itv contienne un booleen faux (entier nul). *)