diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-29 09:17:26 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-29 09:17:26 +0200 |
| commit | 2e39ecb491bbd001ecdfba73115bc76e3f53f517 (patch) | |
| tree | 7925ef9241e8b6d2a42dafe979010230ad36a84f /kvx/Asmgenproof.v | |
| parent | 1bb219c2df5f7b06227a2bddfc24721a372847ab (diff) | |
| download | compcert-kvx-2e39ecb491bbd001ecdfba73115bc76e3f53f517.tar.gz compcert-kvx-2e39ecb491bbd001ecdfba73115bc76e3f53f517.zip | |
Improving the coqdoc
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. |