From f3250c32ff42ae18fd03a5311c1f0caec3415aba Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Jun 2012 08:49:06 +0000 Subject: 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 --- common/Values.v | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'common') 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. -- cgit v1.2.3