diff options
-rw-r--r-- | Makefile | 1 | ||||
-rw-r--r-- | backend/Inject.v | 6 |
2 files changed, 5 insertions, 2 deletions
@@ -86,6 +86,7 @@ BACKEND=\ Kildall.v Liveness.v \ ValueDomain.v ValueAOp.v ValueAnalysis.v \ ConstpropOp.v Constprop.v ConstpropOpproof.v Constpropproof.v \ + Inject.v \ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ diff --git a/backend/Inject.v b/backend/Inject.v index dd70556a..66ef9ce8 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -2,6 +2,8 @@ Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. Require Import AST Linking. Require Import Memory Registers Op RTL. +Local Open Scope positive. + Inductive inj_instr : Type := | INJop: operation -> list reg -> reg -> inj_instr | INJload: memory_chunk -> addressing -> list reg -> reg -> inj_instr. @@ -33,7 +35,7 @@ Definition successor (i : instruction) : node := | Icond _ _ pc' _ => pc' | Itailcall _ _ _ | Ijumptable _ _ - | Ireturn _ => 1%positive + | Ireturn _ => 1 end. Definition alter_successor (i : instruction) (pc' : node) : instruction := @@ -56,5 +58,5 @@ Definition inject_at (prog : code) (pc extra_pc : node) | Some i => inject_list (PTree.set pc (alter_successor i extra_pc) prog) extra_pc (successor i) l - | None => inject_list prog extra_pc 1%positive l (* does not happen *) + | None => inject_list prog extra_pc 1 l (* does not happen *) end. |