From fd00d28f8065acf9b09a6510e1612a91e30ca29c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 10:12:09 +0200 Subject: more on injection --- backend/Inject.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'backend/Inject.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. -- cgit