diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-04-09 09:39:46 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-04-09 09:39:46 +0200 |
| commit | 1a12e99fcc6c2c1ff3cca70612f3c98493743c68 (patch) | |
| tree | e931caeddfe48da23a6276f6fd4e84d6742fcecc /backend/Linearizeaux.ml | |
| parent | e326ed9f28a2ed6869f0cb356ef9a8e189cb0a47 (diff) | |
| download | compcert-kvx-1a12e99fcc6c2c1ff3cca70612f3c98493743c68.tar.gz compcert-kvx-1a12e99fcc6c2c1ff3cca70612f3c98493743c68.zip | |
Removed the assertion about prediction on ifso
Diffstat (limited to 'backend/Linearizeaux.ml')
| -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 |