Changements mineurs Asmblock.v + draft de Asmblockgen.v à compléter

Asmblock.v:
  - Rajout de "header" dans wf_bblock
  - Remplacer "code" par "bblocks". Pour la suite, je trouve plus clair
    de manipuler des bblocks, plutôt qu'un "code constitué de bblocks".
    ça permet de minimiser les modifications dans Asmblockgen.v
  - fn_code --> fn_blocks . fn_code ne devrait pas être utilisé dans le
    code OCaml de toute façon (vu la translation Asmblock -> Asm)
  - Rajout d'un type instruction qui regroupe les basic et les control ;
    facilite certaines définitions

Asmblockgen.v:
  - Copie conforme de Asmgen.v, avec quelques changements (pas fini). Ce
    vers quoi je m'oriente : garder les fonctions existantes de
    génération de code ; on leur donne à manger la liste de basics de
    Machblock. On traduit le exit (qui peut spiller sur la liste de
    basics déjà traduite), et on met la dernière instruction de la trad
    du exit (qui doit être un control) dans le exit du bblock.
  - Pour le prologue : chaque instruction rajoutée "à la main" est dans
    son propre bblock. Voir la notation ::b pour le faire. A terme, il
    devrait y avoir moyen "d'accumuler" l'instruction au code généré ;
    pour l'instant je préfère ne pas compliquer la génération.

1 files changed, 1 insertions, 0 deletions

diff --git a/Makefile b/Makefile
index c9008b23..a9cda92c 100644
--- a/Makefile
+++ b/Makefile
@@ -96,6 +96,7 @@ BACKEND=\
   Mach.v \
   Bounds.v Stacklayout.v Stacking.v Stackingproof.v \
   Machblock.v Machblockgen.v Machblockgenproof.v \
+  Asmblock.v \
   Asm.v Asmgen.v Asmgenproof0.v Asmgenproof1.v Asmgenproof.v
 
 # C front-end modules (in cfrontend/)