diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-06 13:49:48 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-06 13:49:48 +0100 |
| commit | e2c64b54bf5df0927c684a70167378c91cba0ff4 (patch) | |
| tree | 800ae3b857290efa6f3fb1730e678c195aadc405 /backend/Duplicateproof.v | |
| parent | 98764278b804517f733982071da37769816a4833 (diff) | |
| download | compcert-kvx-e2c64b54bf5df0927c684a70167378c91cba0ff4.tar.gz compcert-kvx-e2c64b54bf5df0927c684a70167378c91cba0ff4.zip | |
make it compile for ARM
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index e66a1068..ebb17774 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -392,21 +392,21 @@ Proof. destruct DUPLIC as (i' & H2 & H3). inv H3. pose symbols_preserved as SYMPRES. eexists. split. - + eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto. + + eapply exec_Iload; eauto; (* is the follow still needed?*) erewrite eval_addressing_preserved; eauto. + econstructor; eauto. (* Iload notrap1 *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. pose symbols_preserved as SYMPRES. eexists. split. - + eapply exec_Iload_notrap1; eauto. erewrite eval_addressing_preserved; eauto. + + eapply exec_Iload_notrap1; eauto; erewrite eval_addressing_preserved; eauto. + econstructor; eauto. (* Iload notrap2 *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. pose symbols_preserved as SYMPRES. eexists. split. - + eapply exec_Iload_notrap2; eauto. erewrite eval_addressing_preserved; eauto. + + eapply exec_Iload_notrap2; eauto; erewrite eval_addressing_preserved; eauto. + econstructor; eauto. (* Istore *) @@ -414,7 +414,7 @@ Proof. destruct DUPLIC as (i' & H2 & H3). inv H3. pose symbols_preserved as SYMPRES. eexists. split. - + eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto. + + eapply exec_Istore; eauto; erewrite eval_addressing_preserved; eauto. + econstructor; eauto. (* Icall *) - eapply dupmap_correct in DUPLIC; eauto. |