Make min_int / -1 and min_int % -1 semantically undefined

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1919 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 12 insertions, 4 deletions

diff --git a/common/Values.v b/common/Values.v
index 1e274ad..f0b125a 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -218,14 +218,20 @@ Definition mul (v1 v2: val): val :=
 Definition divs (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then None else Some(Vint(Int.divs n1 n2))
+      if Int.eq n2 Int.zero
+      || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
+      then None
+      else Some(Vint(Int.divs n1 n2))
   | _, _ => None
   end.
 
 Definition mods (v1 v2: val): option val :=
   match v1, v2 with
   | Vint n1, Vint n2 =>
-      if Int.eq n2 Int.zero then None else Some(Vint(Int.mods n1 n2))
+      if Int.eq n2 Int.zero
+      || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
+      then None
+      else Some(Vint(Int.mods n1 n2))
   | _, _ => None
   end.
 
@@ -656,7 +662,8 @@ Theorem mods_divs:
   mods x y = Some z -> exists v, divs x y = Some v /\ z = sub x (mul v y).
 Proof.
   intros. destruct x; destruct y; simpl in *; try discriminate.
-  destruct (Int.eq i0 Int.zero); inv H. 
+  destruct (Int.eq i0 Int.zero
+        || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H.
   exists (Vint (Int.divs i i0)); split; auto. 
   simpl. rewrite Int.mods_divs. auto.
 Qed.
@@ -679,7 +686,8 @@ Theorem divs_pow2:
   shrx x (Vint logn) = Some y.
 Proof.
   intros; destruct x; simpl in H1; inv H1.
-  destruct (Int.eq n Int.zero); inv H3. 
+  destruct (Int.eq n Int.zero
+         || Int.eq i (Int.repr Int.min_signed) && Int.eq n Int.mone); inv H3.
   simpl. rewrite H0. decEq. decEq. symmetry. apply Int.divs_pow2. auto.
 Qed.