Skip to content

Commit 0c6d1af

Browse files
committed
Document interval div
1 parent a0c00fd commit 0c6d1af

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

src/cdomain/value/cdomains/intDomain0.ml

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -361,6 +361,12 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct
361361
let y2p = Ints_t.shift_left Ints_t.one y2 in
362362
mul (x1, x2) (y1p, y2p)
363363

364+
(** Divide mathematical intervals.
365+
Excludes 0 from denominator - must be handled as desired by caller.
366+
367+
@return negative and positive denominator cases separately, if they exist.
368+
369+
@see <https://mine.perso.lip6.fr/publi/article-mine-FTiPL17.pdf> Miné, A. Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation. Figure 4.6. *)
364370
let div (a, b) (c, d) =
365371
let pos =
366372
if Ints_t.(compare one d) <= 0 then

0 commit comments

Comments
 (0)