diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 18:46:50 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 18:46:50 +0200 |
| commit | 27c8e10f4e0a3eee6bf9feb03d0f12990f74badd (patch) | |
| tree | 7761f2d1e53a8d4bd0c47d0b40411c46c1bfe3ad /backend/Inject.v | |
| parent | b937a4c10226930b7109ae6c9707255e53a0dd2b (diff) | |
| download | compcert-kvx-27c8e10f4e0a3eee6bf9feb03d0f12990f74badd.tar.gz compcert-kvx-27c8e10f4e0a3eee6bf9feb03d0f12990f74badd.zip | |
use inject_l
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). +*) |