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/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index c0a04f0b..0f06703c 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -112,8 +112,12 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Orsubshift s, I n1 :: I n2 :: nil => I(Int.sub (eval_static_shift s n2) n1)
   | Orsubimm n, I n1 :: nil => I (Int.sub n n1)
   | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
-  | Odiv, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divs n1 n2)
-  | Odivu, I n1 :: I n2 :: nil => if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
+  | Odiv, I n1 :: I n2 :: nil =>
+      if Int.eq n2 Int.zero then Unknown else
+      if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
+      else I(Int.divs n1 n2)
+  | Odivu, I n1 :: I n2 :: nil =>
+      if Int.eq n2 Int.zero then Unknown else I(Int.divu n1 n2)
   | Oand, I n1 :: I n2 :: nil => I(Int.and n1 n2)
   | Oandshift s, I n1 :: I n2 :: nil => I(Int.and n1 (eval_static_shift s n2))
   | Oandimm n, I n1 :: nil => I(Int.and n1 n)