From 27c8e10f4e0a3eee6bf9feb03d0f12990f74badd Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 18:46:50 +0200 Subject: use inject_l --- backend/Inject.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'backend/Inject.v') 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). +*) -- cgit