diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 16:30:44 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 16:30:44 +0100 |
| commit | 04a46f516487557df00f43453c8decbc8567c458 (patch) | |
| tree | 4ec5bcbbef0ff74ef3923b0f8d1bec8fedf3be75 /backend/Duplicateaux.ml | |
| parent | 361977d47b586dc2f8dec71f597e7f802de8dffa (diff) | |
| download | compcert-kvx-04a46f516487557df00f43453c8decbc8567c458.tar.gz compcert-kvx-04a46f516487557df00f43453c8decbc8567c458.zip | |
Modified the hook for the oracle
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 f86cf39b..38b3ee23 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), []) |