diff options
Diffstat (limited to 'backend/Duplicateaux.ml')
| -rw-r--r-- | backend/Duplicateaux.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 217ba1b2..498cc2c5 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -219,11 +219,21 @@ let get_loop_info is_loop_header bfs_order code = match rtl_successors inst with | [] -> false | [s] -> explore s dest - | [s1; s2] -> begin + | [s1; s2] -> let snapshot_visited = ref !visited in begin (* Remembering that we tried the ifso node *) cb_info := PTree.set src true !cb_info; match explore s1 dest with - | true -> true + | true -> ( + visited := !snapshot_visited; + match explore s2 dest with + | true -> begin + (* Both paths lead to a loop: we cannot predict the CB + * (but the explore still succeeds) *) + cb_info := PTree.remove src !cb_info; + true + end + | false -> true (* nothing to do, the explore succeeded *) + ) | false -> begin cb_info := PTree.set src false !cb_info; match explore s2 dest with |