diff options
Diffstat (limited to 'arm/ConstpropOpproof.v')
| -rw-r--r-- | arm/ConstpropOpproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 242f29b..4c38d5e 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -138,7 +138,8 @@ Proof. rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto. rewrite Val.sub_add_opp. rewrite Val.add_assoc. rewrite Int.sub_add_opp. auto. rewrite Int.sub_add_opp. rewrite shift_symbol_address. rewrite Val.sub_add_opp. auto. - destruct (Int.eq n2 Int.zero); inv H0. simpl; auto. + destruct (Int.eq n2 Int.zero). inv H0. + destruct (Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); inv H0; simpl; auto. destruct (Int.eq n2 Int.zero); inv H0. simpl; auto. destruct (Int.ltu n2 Int.iwordsize); simpl; auto. destruct (Int.ltu n2 Int.iwordsize); simpl; auto. |