diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 17:07:30 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 17:07:30 +0200 |
| commit | ec0a14d34547d0c9ffaf080841570374bd00f3bb (patch) | |
| tree | f3b0feb8f6e5391a6380235e4fbfe00db678f614 | |
| parent | a908ebe6567b06ce2b642851354164fea902fdf8 (diff) | |
| parent | 0192b7df66393bca3f466003112f68e4ae34716a (diff) | |
| download | vericert-kvx-ec0a14d34547d0c9ffaf080841570374bd00f3bb.tar.gz vericert-kvx-ec0a14d34547d0c9ffaf080841570374bd00f3bb.zip | |
Merge remote-tracking branch 'james/develop' into develop
| -rw-r--r-- | src/translation/HTLgenproof.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index f6b90cb..0c79769 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -1477,18 +1477,19 @@ Section CORRECTNESS. rewrite Integers.Ptrofs.add_zero_l. rewrite Integers.Ptrofs.unsigned_repr. simpl. + rewrite HeqOFFSET in *. simplify_val. destruct (Z_le_gt_dec (4 * ptr + 4) (Integers.Ptrofs.unsigned OFFSET)); eauto. + rewrite HeqOFFSET in *. simplify_val. + left; auto. + rewrite HeqOFFSET in *. simplify_val. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. rewrite Z2Nat.id in H16; try lia. apply Zmult_lt_compat_r with (p := 4) in H16; try lia. rewrite ZLib.div_mul_undo in H16; try lia. - rewrite HeqOFFSET in MOD_PRESERVE. apply MOD_PRESERVE. - rewrite HeqOFFSET in n. apply n. - admit. admit. admit. - (*split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia.*) + split; try lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } rewrite <- EXPR_OK. |