diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-03-01 13:52:05 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-03-01 13:52:05 +0100 |
| commit | ab776cd94e000d07c4d14521a8d0c635d3b8412c (patch) | |
| tree | 22555b05913252c3c6d9583f405905914c5a781b /kvx/NeedOp.v | |
| parent | b0c6449c57a92fa0ba67dd7c9a98ffcc8e5d8bb6 (diff) | |
| parent | 916f120316108f1db9537eccb5151e7b59f82a1f (diff) | |
| download | compcert-kvx-ab776cd94e000d07c4d14521a8d0c635d3b8412c.tar.gz compcert-kvx-ab776cd94e000d07c4d14521a8d0c635d3b8412c.zip | |
Merge remote-tracking branch 'origin/kvx-work' into merge_absint
Diffstat (limited to 'kvx/NeedOp.v')
| -rw-r--r-- | kvx/NeedOp.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v index 4578b4e8..cc86fc88 100644 --- a/kvx/NeedOp.v +++ b/kvx/NeedOp.v @@ -137,6 +137,10 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Osel c ty => nv :: nv :: needs_of_condition0 c | Oselimm c imm | Osellimm c imm => nv :: needs_of_condition0 c + | Oabsdiff => op2 (default nv) + | Oabsdiffimm _ => op1 (default nv) + | Oabsdiffl => op2 (default nv) + | Oabsdifflimm _ => op1 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := |