diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 09:08:15 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 09:08:15 +0100 |
| commit | 35a17f7c9a42e654a646114aeecfbba60fd71b06 (patch) | |
| tree | df5462a0a80063ac92eb85a8c23ab5bf9fe3f259 /backend/ForwardMoves.v | |
| parent | 36f336d8c57f053342ec794e5bc802ebb66fc82b (diff) | |
| download | compcert-kvx-35a17f7c9a42e654a646114aeecfbba60fd71b06.tar.gz compcert-kvx-35a17f7c9a42e654a646114aeecfbba60fd71b06.zip | |
moving forward with proofs
Diffstat (limited to 'backend/ForwardMoves.v')
| -rw-r--r-- | backend/ForwardMoves.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index 660d0458..e820723c 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -251,13 +251,14 @@ Definition apply_instr instr x := match instr with | Inop _ | Icond _ _ _ _ - | Istore _ _ _ _ _ => Some x + | Ijumptable _ _ + | Istore _ _ _ _ _ + | Icall _ _ _ _ _ => Some x | Iop Omove (src :: nil) dst _ => Some (move src dst x) | Iop _ _ dst _ - | Iload _ _ _ _ dst _ - | Icall _ _ _ dst _ => Some (kill dst x) + | Iload _ _ _ _ dst _=> Some (kill dst x) | Ibuiltin _ _ res _ => Some (kill_builtin_res res x) - | Itailcall _ _ _ | Ijumptable _ _ | Ireturn _ => RB.bot + | Itailcall _ _ _ | Ireturn _ => RB.bot end. Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := |