From 535a8f8706de231f1bd8a7f0243025d84906b03c Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 3 Nov 2020 15:06:45 +0100 Subject: Loop Rotate with -flooprotate --- backend/Duplicatepasses.v | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'backend/Duplicatepasses.v') 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. -- cgit