diff options
| author | nicolas.nardino <nicolas.nardino@ens-lyon.fr> | 2021-06-06 12:11:15 +0200 |
|---|---|---|
| committer | nicolas.nardino <nicolas.nardino@ens-lyon.fr> | 2021-06-06 12:11:15 +0200 |
| commit | 9118878bd14e24cc04c2f36cab7aa7271a0f1852 (patch) | |
| tree | f7a6f1a32fc6bab218892e18f38a887fe6a84db9 | |
| parent | 599823a6410f1629f2b8704291839e0974bce83b (diff) | |
| download | compcert-kvx-9118878bd14e24cc04c2f36cab7aa7271a0f1852.tar.gz compcert-kvx-9118878bd14e24cc04c2f36cab7aa7271a0f1852.zip | |
Fixing scope error, and non-exhaustive pattern matching
| -rw-r--r-- | scheduling/RTLpathScheduleraux.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml index 5a427e6c..653765f5 100644 --- a/scheduling/RTLpathScheduleraux.ml +++ b/scheduling/RTLpathScheduleraux.ml @@ -96,15 +96,15 @@ let get_live_regs_entry (sb : superblock) code = | Icall (_, fn, args, dest, _) -> List.fold_left (fun set reg -> Registers.Regset.add reg set) ((match fn with - | Coq_inl reg -> (Registers.Regset.add reg) - | Coq_inr _ -> (fun x -> x)) + | Datatypes.Coq_inl reg -> (Registers.Regset.add reg) + | Datatypes.Coq_inr _ -> (fun x -> x)) (Registers.Regset.remove dest regset)) args | Itailcall (_, fn, args) -> List.fold_left (fun set reg -> Registers.Regset.add reg set) (match fn with - | Coq_inl reg -> (Registers.Regset.add reg regset) - | Coq_inr _ -> regset) + | Datatypes.Coq_inl reg -> (Registers.Regset.add reg regset) + | Datatypes.Coq_inr _ -> regset) args | Ibuiltin (_, args, dest, _) -> List.fold_left (fun set reg -> @@ -112,7 +112,8 @@ let get_live_regs_entry (sb : superblock) code = | AST.BA r -> Registers.Regset.add r set | _ -> set) (match dest with - | AST.BR r -> Registers.Regset.remove r regset) + | AST.BR r -> Registers.Regset.remove r regset + | _ -> regset) args | Icond (_, args, _, _, _) -> List.fold_left (fun set reg -> |