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