diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:48 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:48 +0100 |
| commit | 903ed0cfa5cb91d99ee373fc8cf408c0a80f968a (patch) | |
| tree | aa2c764c4269a42e4a947182f1a76c3585cc15d3 /backend/Duplicateaux.ml | |
| parent | 1acafe8f7f61a8908f47de4c98f3d873f8f9afbd (diff) | |
| download | compcert-kvx-903ed0cfa5cb91d99ee373fc8cf408c0a80f968a.tar.gz compcert-kvx-903ed0cfa5cb91d99ee373fc8cf408c0a80f968a.zip | |
Revert "Modified the hook for the oracle"
This reverts commit 04a46f516487557df00f43453c8decbc8567c458.
It was actually not needed
Diffstat (limited to 'backend/Duplicateaux.ml')
| -rw-r--r-- | backend/Duplicateaux.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 38b3ee23..f86cf39b 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -541,4 +541,4 @@ let duplicate_aux f = let traces = select_traces (to_ttl_code code entrypoint) entrypoint in let preds = get_predecessors_rtl code in let (new_code, pTreeId) = (print_traces traces; superblockify_traces code preds traces) in - (((new_code, (fn_entrypoint f)), pTreeId), []) + ((new_code, (fn_entrypoint f)), pTreeId) |