diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 17:40:52 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 17:40:52 +0100 |
| commit | fb5029eb72a3a28b26f3d982c30badc8d027f405 (patch) | |
| tree | a1df65bdddfafff619c50f4e7bd113f2146713b5 /backend/ForwardMoves.v | |
| parent | 2e79fb4d9bb98f497d59cf52ca3df5cc90515d53 (diff) | |
| download | compcert-kvx-fb5029eb72a3a28b26f3d982c30badc8d027f405.tar.gz compcert-kvx-fb5029eb72a3a28b26f3d982c30badc8d027f405.zip | |
fix move
Diffstat (limited to 'backend/ForwardMoves.v')
| -rw-r--r-- | backend/ForwardMoves.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index 4cc9d5bc..c73b0213 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -238,7 +238,7 @@ Definition move (src dst : reg) (rel : RELATION.t) := PTree.set dst (match PTree.get src rel with | Some src' => src' | None => src - end) rel. + end) (kill dst rel). Fixpoint kill_builtin_res (res : builtin_res reg) (rel : RELATION.t) := match res with @@ -257,7 +257,7 @@ Definition apply_instr instr x := | Iop _ _ dst _ | Iload _ _ _ _ dst _ | Icall _ _ _ dst _ => Some (kill dst x) - | Ibuiltin _ _ res _ => Some (kill_builtin_res res x) + | Ibuiltin _ _ res _ => Some (RELATION.top) (* TODO (kill_builtin_res res x) *) | Itailcall _ _ _ | Ireturn _ => RB.bot end. |