diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-23 18:13:28 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-23 18:13:28 +0100 |
| commit | a78fe0efa4b114d7c5ae11d0bed8cd17d55fd89c (patch) | |
| tree | c8a59f14c27caf63241c507e7a7ff023c55c4c8a /scheduling/RTLpathWFcheck.v | |
| parent | 3ce99d1f53b24704b45b6984d0fd0bc156016309 (diff) | |
| parent | 91699fd379eb4087eb4088af77a5eb918552dc5e (diff) | |
| download | compcert-kvx-a78fe0efa4b114d7c5ae11d0bed8cd17d55fd89c.tar.gz compcert-kvx-a78fe0efa4b114d7c5ae11d0bed8cd17d55fd89c.zip | |
Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-work
Diffstat (limited to 'scheduling/RTLpathWFcheck.v')
| -rw-r--r-- | scheduling/RTLpathWFcheck.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v index 0ddc3142..63b914ec 100644 --- a/scheduling/RTLpathWFcheck.v +++ b/scheduling/RTLpathWFcheck.v @@ -31,14 +31,13 @@ Proof. inversion_SOME path; try_simplify_someHyps. Qed. -(* FIXME - what about trap? *) Definition iinst_checker (pm: path_map) (i: instruction): option (node) := match i with | Inop pc' | Iop _ _ _ pc' | Iload _ _ _ _ _ pc' | Istore _ _ _ _ pc' => Some (pc') | Icond cond args ifso ifnot _ => exit_checker pm ifso ifnot - | _ => None (* TODO jumptable ? *) + | _ => None end. Local Hint Resolve exit_checker_path_entry: core. |