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

3 files changed, 14 insertions, 8 deletions

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index f725662..9de6b32 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1459,11 +1459,13 @@ Proof.
     rewrite zeq_true. rewrite Int.sub_shifted. auto.
   inv H; inv H0; inv H1; TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
-    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
+    destruct (Int.eq i0 Int.zero
+      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
     destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
-    destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
+    destruct (Int.eq i0 Int.zero
+      || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H; TrivialExists.
   inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
     destruct (Int.eq i0 Int.zero); inv H. TrivialExists.
   inv H; inv H0; inv H1; TrivialExists.
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 9087aa4..ac7a58f 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -300,7 +300,9 @@ Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   | div_case_ii Signed =>
       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
   | div_case_ff =>
@@ -333,7 +335,9 @@ Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   | binint_case_ii Signed =>
       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
   | binint_default =>
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 37f15cf..76f08f3 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -367,15 +367,15 @@ Proof.
   unfold sem_mul in *. destruct (classify_mul ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
 (* div *)
   unfold sem_div in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0.
-  rewrite H11 in H2. inv H2. inv H12. constructor.
-  rewrite H11 in H2. inv H2. inv H12. constructor.
+  inv H12. rewrite H11 in H2. inv H2. constructor.
+  inv H12. rewrite H11 in H2. inv H2. constructor.
   inv H11. constructor.
   inv H11. constructor.
   inv H11. constructor.
 (* mod *)
   unfold sem_mod in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0.
-  rewrite H11 in H2. inv H2. inv H12. constructor.
-  rewrite H11 in H2. inv H2. inv H12. constructor.
+  inv H12. rewrite H11 in H2. inv H2. constructor.
+  inv H12. rewrite H11 in H2. inv H2. constructor.
 (* and *)
   unfold sem_and in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
 (* or *)