diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 14:57:24 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-10 14:57:24 +0100 |
| commit | c2319ee007eba06f92837e1e370dfa5e58b06b82 (patch) | |
| tree | 1ba3aee545d6ee3f0439c8830e69858bdb1ee15b /backend/CSE3analysis.v | |
| parent | b00665af60dc019c75e0f2a64099db163b4c3c26 (diff) | |
| download | compcert-kvx-c2319ee007eba06f92837e1e370dfa5e58b06b82.tar.gz compcert-kvx-c2319ee007eba06f92837e1e370dfa5e58b06b82.zip | |
oper2
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 41fa67f6..456898cf 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -216,6 +216,16 @@ Section OPERATIONS. else None end end. -End OPERATIONS. + + Definition oper2 (no : node) (dst : reg) (op: sym_op)(args : list reg) + (rel : RELATION.t) := + let rel' := kill_reg dst rel in + match eq_find no {| eq_lhs := dst; + eq_op := op; + eq_args:= args |} with + | Some id => PSet.add id rel' + | None => rel' + end. + End OPERATIONS. Definition totoro := RELATION.lub. |