diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-11-03 15:06:45 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-11-03 15:06:45 +0100 |
| commit | 535a8f8706de231f1bd8a7f0243025d84906b03c (patch) | |
| tree | 5a4def9024c63d318de6b716bab83523b983961a /backend/Duplicatepasses.v | |
| parent | e6612fdfd69037099037def2acba5df553c3b49a (diff) | |
| download | compcert-kvx-535a8f8706de231f1bd8a7f0243025d84906b03c.tar.gz compcert-kvx-535a8f8706de231f1bd8a7f0243025d84906b03c.zip | |
Loop Rotate with -flooprotate
Diffstat (limited to 'backend/Duplicatepasses.v')
| -rw-r--r-- | backend/Duplicatepasses.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v index dc96f966..7e58eedf 100644 --- a/backend/Duplicatepasses.v +++ b/backend/Duplicatepasses.v @@ -45,4 +45,14 @@ End TailDuplicateOracle. Module Tailduplicateproof := DuplicateProof TailDuplicateOracle. -Module Tailduplicate := Tailduplicateproof.
\ No newline at end of file +Module Tailduplicate := Tailduplicateproof. + +(** Loop Rotate *) + +Module LoopRotateOracle <: DuplicateOracle. + Axiom duplicate_aux : function -> code * node * (PTree.t node). + Extract Constant duplicate_aux => "Duplicateaux.loop_rotate". +End LoopRotateOracle. + +Module Looprotateproof := DuplicateProof LoopRotateOracle. +Module Looprotate := Looprotateproof. |