diff options
| author | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-06-01 10:13:41 +0200 |
|---|---|---|
| committer | Alex AUVOLAT <alex.auvolat@ens.fr> | 2014-06-01 10:13:41 +0200 |
| commit | 727354805f3c33d17bff18b74fc688b631e85f41 (patch) | |
| tree | a6c5eb95d93fb045d8c0795d9c8d213252cab4b6 /abstract | |
| parent | 652d04c5476fdfb9cc7a2d93de3df4d76a6882ce (diff) | |
| download | SemVerif-Projet-727354805f3c33d17bff18b74fc688b631e85f41.tar.gz SemVerif-Projet-727354805f3c33d17bff18b74fc688b631e85f41.zip | |
Assert j != 0 in bound_div i j
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/intervals_domain.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index d95a938..06c5e57 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -43,10 +43,8 @@ module Intervals : VALUE_DOMAIN = struct if i < Z.zero then PInf else MInf | Int i, Int j -> - if j = Z.zero then - if i < Z.zero then MInf - else PInf - else Int (Z.div i j) + assert (j != Z.zero); + Int (Z.div i j) let bound_min a b = match a, b with @@ -116,8 +114,6 @@ module Intervals : VALUE_DOMAIN = struct (bound_min (bound_mul b c) (bound_mul b d))), (bound_max (bound_max (bound_mul a c) (bound_mul a d)) (bound_max (bound_mul b c) (bound_mul b d)))) - - let div a b = match a, b with | Bot, _ -> Bot | Itv(a, b), q -> @@ -132,7 +128,6 @@ module Intervals : VALUE_DOMAIN = struct Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d)) in join p1 p2 - let rem a b = match a, b with | Bot, _ | _, Bot -> Bot | Itv(a, b), Itv(c, d) -> |