diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 10:12:09 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 10:12:09 +0200 |
| commit | fd00d28f8065acf9b09a6510e1612a91e30ca29c (patch) | |
| tree | 323df3891fdf06ee6bec7a9c38fb562b71b5dc3a /backend/Inject.v | |
| parent | 4aad20a92dc926d8c537e65946ca03bf2b6b02b9 (diff) | |
| download | compcert-kvx-fd00d28f8065acf9b09a6510e1612a91e30ca29c.tar.gz compcert-kvx-fd00d28f8065acf9b09a6510e1612a91e30ca29c.zip | |
more on injection
Diffstat (limited to 'backend/Inject.v')
| -rw-r--r-- | backend/Inject.v | 6 |
1 files changed, 4 insertions, 2 deletions
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. |