diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-14 22:41:24 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-14 22:41:24 +0200 |
commit | 4c146156a36d48209a6206f61f80dc5d4c48ce93 (patch) | |
tree | dc8e3b1c7daf41cdf965c9e3e6119dcb5d6a41e5 /cfrontend/Cop.v | |
parent | d03d47c6e4ce9324d6d59ae36cb8db78b013be54 (diff) | |
parent | f995a671ceb28c2a83e5e5574c3cdb46fd5e0f57 (diff) | |
download | compcert-4c146156a36d48209a6206f61f80dc5d4c48ce93.tar.gz compcert-4c146156a36d48209a6206f61f80dc5d4c48ce93.zip |
Merge branch 'master' into asmexpand
Diffstat (limited to 'cfrontend/Cop.v')
-rw-r--r-- | cfrontend/Cop.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index 6284660c..948ccaca 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -709,8 +709,10 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type) match v1,v2 with | Vptr b1 ofs1, Vptr b2 ofs2 => if eq_block b1 b2 then - if Int.eq (Int.repr (sizeof cenv ty)) Int.zero then None - else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof cenv ty)))) + let sz := sizeof cenv ty in + if zlt 0 sz && zle sz Int.max_signed + then Some (Vint (Int.divs (Int.sub ofs1 ofs2) (Int.repr sz))) + else None else None | _, _ => None end @@ -1216,7 +1218,7 @@ Proof. + inv H0; inv H1; inv H. TrivialInject. destruct (eq_block b1 b0); try discriminate. subst b1. rewrite H0 in H2; inv H2. rewrite dec_eq_true. - destruct (Int.eq (Int.repr (sizeof cenv ty)) Int.zero); inv H3. + destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3. rewrite Int.sub_shifted. TrivialInject. + inv H0; inv H1; inv H. TrivialInject. econstructor. eauto. rewrite Int.sub_add_l. auto. |