diff options
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. |