diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-02-22 16:09:53 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-02-22 16:09:53 +0100 |
| commit | b0452edc5e911d8585a691ad4e530d4f1427f463 (patch) | |
| tree | 8431c2d1b18941033e13ae2db7cf182e11ee6762 /scheduling/RTLpathSE_impl.v | |
| parent | 8faafc7668b9423ba9bee1f4e725eab5b378c851 (diff) | |
| download | compcert-kvx-b0452edc5e911d8585a691ad4e530d4f1427f463.tar.gz compcert-kvx-b0452edc5e911d8585a691ad4e530d4f1427f463.zip | |
a bit more cleaning
Diffstat (limited to 'scheduling/RTLpathSE_impl.v')
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index bd26171d..bdd4bda8 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -764,7 +764,7 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) : DO vargs <~ hlist_args prev args ;; let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |}) - | _ => RET None (* TODO jumptable ? *) + | _ => RET None end. |