diff options
Diffstat (limited to 'backend/ValueAnalysis.v')
| -rw-r--r-- | backend/ValueAnalysis.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 08adff2b..3c3aecfd 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -100,9 +100,9 @@ Definition transfer_builtin let p := loadbytes am rm (aptr_of_aval asrc) in let am' := storebytes am (aptr_of_aval adst) sz p in VA.State (set_builtin_res res ntop ae) am' - | (EF_annot _ _ | EF_debug _ _ _), _ => + | (EF_annot _ _ _ | EF_debug _ _ _), _ => VA.State (set_builtin_res res ntop ae) am - | EF_annot_val _ _, v :: nil => + | EF_annot_val _ _ _, v :: nil => let av := abuiltin_arg ae am rm v in VA.State (set_builtin_res res av ae) am | _, _ => @@ -876,7 +876,7 @@ Proof. apply smatch_ge with Nonstack. eapply SM. eapply mmatch_top; eauto. apply pge_lub_r. + (* below *) red; simpl; intros. destruct (eq_block b sp). - subst b. apply Plt_le_trans with bound. apply BELOW. congruence. auto. + subst b. apply Pos.lt_le_trans with bound. apply BELOW. congruence. auto. eapply mmatch_below; eauto. - (* genv *) eapply genv_match_exten; eauto. @@ -1009,7 +1009,7 @@ Proof. + apply SMTOP; auto. + apply SMTOP; auto. + red; simpl; intros. destruct (plt b (Mem.nextblock m)). - eapply Plt_le_trans. eauto. eapply external_call_nextblock; eauto. + eapply Pos.lt_le_trans. eauto. eapply external_call_nextblock; eauto. destruct (j' b) as [[bx deltax] | ] eqn:J'. eapply Mem.valid_block_inject_1; eauto. congruence. |