From bae72eeffdd23c3444a097f5f901333c6c70af8b Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 30 Mar 2020 10:59:38 +0200 Subject: more on injection --- backend/Inject.v | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'backend/Inject.v') diff --git a/backend/Inject.v b/backend/Inject.v index 66ef9ce8..a3f2b343 100644 --- a/backend/Inject.v +++ b/backend/Inject.v @@ -60,3 +60,13 @@ Definition inject_at (prog : code) (pc extra_pc : node) extra_pc (successor i) l | None => inject_list prog extra_pc 1 l (* does not happen *) end. + +Definition inject_at' (already : node * code) pc l := + let (extra_pc, prog) := already in + inject_at prog pc extra_pc l. + +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