diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-19 16:46:26 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-20 15:05:56 +0100 |
| commit | f6473ff0069aa6493d6c52a5dd05b460269236e0 (patch) | |
| tree | 62b958747c33b044a7853ed77d0e4d59be49f2f1 /mppa_k1c/Asmblockdeps.v | |
| parent | 06e0295e4b6289a33d456e1b93dea615b65dc755 (diff) | |
| download | compcert-kvx-f6473ff0069aa6493d6c52a5dd05b460269236e0.tar.gz compcert-kvx-f6473ff0069aa6493d6c52a5dd05b460269236e0.zip | |
Problème résolu en prenant les noms de resources comme étant des Pos
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 54258882..934e7d83 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -6,11 +6,13 @@ Require Import Memory. Require Import Errors. Require Import Integers. Require Import Floats. +Require Import ZArith. Require Import ImpDep. Open Scope impure. -Module R<: ResourceNames. +(* FIXME - incompatible with IDP (not without additional code) so commenting it out *) +(* Module R<: ResourceNames. Inductive t_wrap := Reg (r: preg) | Mem. @@ -21,11 +23,10 @@ Proof. decide equality. decide equality; apply ireg_eq. Qed. -End R. - +End R. *) Module P<: ImpParam. -Module R := R. +Module R := Pos. Section IMPPARAM. @@ -339,3 +340,12 @@ Include MkSeqLanguage P. End L. Module IDT := ImpDepTree L ImpPosDict. + +Section SECT. +Variable ge: P.genv. + +(** Compilation from Asmblock to L *) + +(* TODO - d'abord, raffiner le modèle dans PostpassScheduling.v pour extraire le exit (n'envoyer que le body à la vérif) *) + +End SECT. |