diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-01 19:58:42 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-09-01 19:58:42 +0200 |
| commit | d1fe9e79ad19feff22f9e319dfafc36a534d9479 (patch) | |
| tree | d855a9ca03d8958fba4926ee04a849f7895f4c97 /backend/CSE3analysis.v | |
| parent | 74901c6df6ceb92da58ef5db2592fc05561dce01 (diff) | |
| parent | cb4ddeeeaca4736c2baceecec0511f8f99f465fc (diff) | |
| download | compcert-kvx-d1fe9e79ad19feff22f9e319dfafc36a534d9479.tar.gz compcert-kvx-d1fe9e79ad19feff22f9e319dfafc36a534d9479.zip | |
Merge remote-tracking branch 'origin/parameterized-cse3' into kvx-work
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 75e00f67..9a6c9c0d 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -477,13 +477,10 @@ Section OPERATIONS. end. Definition apply_cond cond args (rel : RELATION.t) : RB.t := - if Compopts.optim_CSE3_conditions tt - then - match apply_cond1 cond args rel with + match apply_cond1 cond args rel with | Some rel => Some (apply_cond0 cond args rel) | None => RB.bot - end - else Some rel. + end. Definition apply_instr (tenv : typing_env) (instr : RTL.instruction) (rel : RELATION.t) : list (node * RB.t) := match instr with |