diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-13 16:01:05 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-13 16:01:05 +0200 |
| commit | 5c4985681d98ca7c3c2616e6286ab3274a7dd6c9 (patch) | |
| tree | e1f065bc8aa599ab60e643b304eed98283208a75 /kvx | |
| parent | eea5640e55890538fa43c3d5672853a0ae015b9c (diff) | |
| parent | 5b756533e3fbd51b8b824e9ed87d2be3feff8f36 (diff) | |
| download | compcert-kvx-5c4985681d98ca7c3c2616e6286ab3274a7dd6c9.tar.gz compcert-kvx-5c4985681d98ca7c3c2616e6286ab3274a7dd6c9.zip | |
Merge branch 'mppa-RTLpathSE-oracle' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-oracle
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathScheduleraux.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kvx/lib/RTLpathScheduleraux.ml b/kvx/lib/RTLpathScheduleraux.ml index 7a43fed5..08cda134 100644 --- a/kvx/lib/RTLpathScheduleraux.ml +++ b/kvx/lib/RTLpathScheduleraux.ml @@ -167,7 +167,12 @@ let change_successors i = function | Icall (a,b,c,d,n) -> Icall (a,b,c,d,s) | Ibuiltin (a,b,c,n) -> Ibuiltin (a,b,c,s) | Ijumptable (a,[n]) -> Ijumptable (a,[s]) - | Icond _ -> failwith "Icond Wrong instruction (2)" + | Icond (a,b,n1,n2,p) -> ( + match p with + | Some true -> Icond (a,b,s,n2,p) + | Some false -> Icond (a,b,n1,s,p) + | None -> failwith "Icond Wrong instruction (2) ; should not happen?" + ) | _ -> failwith "Wrong instruction (2)") | [s1; s2] -> ( match i with |