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, 6 insertions, 2 deletions

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 9087aa4c..ac7a58f6 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 =>