diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-03-11 17:00:48 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-03-11 17:00:48 +0100 |
| commit | 3fef5e1d45820a775a7c941851af6f0bf3f1537d (patch) | |
| tree | fc36893a6d590f33bd21ab40e040143793998eaa /backend/Inlining.v | |
| parent | 1b00a75796a8ace42cc480efadaad948407f5a31 (diff) | |
| download | compcert-kvx-3fef5e1d45820a775a7c941851af6f0bf3f1537d.tar.gz compcert-kvx-3fef5e1d45820a775a7c941851af6f0bf3f1537d.zip | |
Adding info field for branching in RTL, LTL, XTL and all associated passes
Diffstat (limited to 'backend/Inlining.v')
| -rw-r--r-- | backend/Inlining.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Inlining.v b/backend/Inlining.v index 9cf535b9..8c7e1898 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -397,9 +397,9 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit := | Ibuiltin ef args res s => set_instr (spc ctx pc) (Ibuiltin ef (map (sbuiltinarg ctx) args) (sbuiltinres ctx res) (spc ctx s)) - | Icond cond args s1 s2 => + | Icond cond args s1 s2 info => set_instr (spc ctx pc) - (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) + (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2) info) | Ijumptable r tbl => set_instr (spc ctx pc) (Ijumptable (sreg ctx r) (List.map (spc ctx) tbl)) |