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 --- ia32/Op.v | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'ia32/Op.v') diff --git a/ia32/Op.v b/ia32/Op.v index 0b32b88e..9fdafe14 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -361,9 +361,11 @@ Proof with (try exact I). destruct v0; destruct v1... simpl. destruct (zeq b b0)... destruct v0; destruct v1... destruct v0... + destruct v0; destruct v1; simpl in *; inv H0. + destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2... destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... - destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... - destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... + destruct v0; destruct v1; simpl in *; inv H0. + destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2... destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2... destruct v0; destruct v1... destruct v0... @@ -837,12 +839,12 @@ Proof. rewrite Int.sub_shifted. auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists. inv H4; inv H3; simpl in H1; inv H1. simpl. destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. - inv H4; inv H3; simpl in H1; inv H1. simpl. - destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. + inv H4; inv H3; simpl in H1; inv H1. simpl. + destruct (Int.eq i0 Int.zero || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists. inv H4; inv H3; simpl in H1; inv H1. simpl. destruct (Int.eq i0 Int.zero); inv H2. TrivialExists. inv H4; inv H2; simpl; auto. -- cgit