diff options
Diffstat (limited to 'backend/Inject.v')
| -rw-r--r-- | backend/Inject.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/backend/Inject.v b/backend/Inject.v index a3f2b343..6799ec8a 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -65,8 +65,15 @@ Definition inject_at' (already : node * code) pc l := let (extra_pc, prog) := already in inject_at prog pc extra_pc l. +Definition inject_l (prog : code) extra_pc injections := + List.fold_left (fun already (injection : node * (list inj_instr)) => + inject_at' already (fst injection) (snd injection)) + injections + (extra_pc, prog). +(* Definition inject' (prog : code) (extra_pc : node) (injections : PTree.t (list inj_instr)) := PTree.fold inject_at' injections (extra_pc, prog). Definition inject prog extra_pc injections : code := snd (inject' prog extra_pc injections). +*) |