diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 09:49:57 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-09 09:49:57 +0200 |
| commit | 3907d3d6029a7d867f5be2c0434a44eeca1d9e46 (patch) | |
| tree | 4c753a995b495d771b1ae9cd15e7438f76d06ecb | |
| parent | faefa6511fc98977e4af3750ca152441284e8186 (diff) | |
| parent | 1a12e99fcc6c2c1ff3cca70612f3c98493743c68 (diff) | |
| download | compcert-kvx-3907d3d6029a7d867f5be2c0434a44eeca1d9e46.tar.gz compcert-kvx-3907d3d6029a7d867f5be2c0434a44eeca1d9e46.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-profiling
| -rw-r--r-- | backend/Linearizeaux.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 1381877b..9d5a5ba6 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -193,8 +193,9 @@ let forward_sequences code entry = if get_some @@ PTree.get ifnot join_points then ([], [ifso; ifnot]) else let ln, rem = traverse_fallthrough code ifnot in (ln, [ifso] @ rem) | Some true -> - let errstr = Printf.sprintf ("Inconsistency detected in node %d: ifnot is not the preferred branch") (P.to_int node) in - failwith errstr) + if get_some @@ PTree.get ifso join_points then ([], [ifso; ifnot]) + else let ln, rem = traverse_fallthrough code ifso in (ln, [ifnot] @ rem) + ) | Ljumptable(_, ln) -> begin (* debug "STOP Ljumptable\n"; *) ([], ln) end in ([node] @ ln, rem) end |