diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-06 12:51:42 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-07-06 12:51:42 +0200 |
commit | e30aa60a06817ed67c14a80430a7275defc41e76 (patch) | |
tree | b4bb512416a40578db1f32eb3a7836ddb6f8582d /cfrontend/Cop.v | |
parent | aa780c7145a418b4a7264e828258034fc4629313 (diff) | |
parent | 2f31c1867b75040067a1ef74ae32f197e8d296c1 (diff) | |
download | compcert-e30aa60a06817ed67c14a80430a7275defc41e76.tar.gz compcert-e30aa60a06817ed67c14a80430a7275defc41e76.zip |
Merge branch 'master' into json_export
Conflicts:
driver/Driver.ml
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. |