diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-12 14:21:18 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-12 14:21:18 +0100 |
commit | 07e482340977d1ee469eed81d0dae25d49e5abe8 (patch) | |
tree | bef4ee12fec1a99c9115d23e119c563911737d1c | |
parent | 81e91f965e7b1afbea8d1630015e75f11f0a3afd (diff) | |
parent | 5aecefe808aaaad6ab05037e7d5e7f53b53e0b94 (diff) | |
download | compcert-07e482340977d1ee469eed81d0dae25d49e5abe8.tar.gz compcert-07e482340977d1ee469eed81d0dae25d49e5abe8.zip |
Merge branch 'master' into dwarf
-rw-r--r-- | backend/ValueAnalysis.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 813944d6..9c7ca1f7 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -186,6 +186,7 @@ Definition alloc_global (rm: romem) (idg: ident * globdef fundef unit): romem := PTree.remove id rm | (id, Gvar v) => if v.(gvar_readonly) && negb v.(gvar_volatile) + && match v.(gvar_init) with nil => false | _ => true end then PTree.set id (store_init_data_list (ablock_init Pbot) 0 v.(gvar_init)) rm else PTree.remove id rm end. @@ -1677,13 +1678,15 @@ Proof. destruct (peq id id1). congruence. eapply H; eauto. - rewrite PTree.gsspec in H0. destruct (peq id id1). + inv H0. rewrite PTree.gss. - destruct (gvar_readonly v1 && negb (gvar_volatile v1)) eqn:RO. - InvBooleans. rewrite negb_true_iff in H2. + destruct (gvar_readonly v1 && negb (gvar_volatile v1) && + match gvar_init v1 with nil => false | _ => true end) eqn:RO. + InvBooleans. rewrite negb_true_iff in H4. rewrite PTree.gss in H1. exists v1. intuition congruence. rewrite PTree.grs in H1. discriminate. + rewrite PTree.gso. eapply H; eauto. - destruct (gvar_readonly v1 && negb (gvar_volatile v1)). + destruct (gvar_readonly v1 && negb (gvar_volatile v1) && + match gvar_init v1 with nil => false | _ => true end). rewrite PTree.gso in H1; auto. rewrite PTree.gro in H1; auto. apply Plt_ne. eapply Genv.genv_symb_range; eauto. |