diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-10 16:21:23 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-10 16:21:23 +0200 |
| commit | 2e54a9c599ef13e4fe84ec80fac4c1835a052241 (patch) | |
| tree | 83c9c98a5ed41f1447edd4089fb9850281bd139e /kvx/Asmgenproof.v | |
| parent | 0566b93d9e42ab023eb95a4535af0c3a86b0421c (diff) | |
| parent | 8d1c157bf4f262de656abfee51afd2f56f8127db (diff) | |
| download | compcert-kvx-2e54a9c599ef13e4fe84ec80fac4c1835a052241.tar.gz compcert-kvx-2e54a9c599ef13e4fe84ec80fac4c1835a052241.zip | |
Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk
Diffstat (limited to 'kvx/Asmgenproof.v')
| -rw-r--r-- | kvx/Asmgenproof.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kvx/Asmgenproof.v b/kvx/Asmgenproof.v index f43acd37..9e35e268 100644 --- a/kvx/Asmgenproof.v +++ b/kvx/Asmgenproof.v @@ -13,7 +13,7 @@ (* *) (* *************************************************************) -(** Correctness proof for Asmgen *) +(** Composing all passes from Mach to KVX Asm *) Require Import Coqlib Errors. Require Import Integers Floats AST Linking. @@ -46,7 +46,7 @@ Proof. exists tp; split. apply Asm.transf_program_match; auto. auto. Qed. -(** Return Address Offset *) +(** Return Address Offset for Mach *) Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop := Mach_return_address_offset Asmblockgenproof.return_address_offset. @@ -59,6 +59,7 @@ Proof. intros; eapply Asmblockgenproof.return_address_exists; eauto. Qed. +(** Main preservation theorem: from Mach to KVX Asm *) Section PRESERVATION. @@ -86,7 +87,7 @@ End PRESERVATION. Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes). (*******************************************) -(* Stub actually needed by driver/Compiler *) +(** Stub actually needed by driver/Compiler *) Module Asmgenproof0. |