diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-10-02 15:14:04 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-10-02 15:14:04 +0200 |
| commit | c22d994917d6a67efc065c1205ede4d448445c10 (patch) | |
| tree | 5ba77154b81fac1b1d08ac5f3b0fc89324564ae1 /backend/Duplicateaux.ml | |
| parent | c5bda24745977119324e97909f491d65a04ac509 (diff) | |
| download | compcert-kvx-c22d994917d6a67efc065c1205ede4d448445c10.tar.gz compcert-kvx-c22d994917d6a67efc065c1205ede4d448445c10.zip | |
Identity oracle realizing verify_mapping_entrypoint
Diffstat (limited to 'backend/Duplicateaux.ml')
| -rw-r--r-- | backend/Duplicateaux.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index a272ac85..70726c4a 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -1,4 +1,7 @@ open RTL open Maps -let duplicate_aux f = (((fn_code f), (fn_entrypoint f)), PTree.empty) +(* For now, identity function *) +let duplicate_aux f = + let pTreeEntry = PTree.set (fn_entrypoint f) (fn_entrypoint f) PTree.empty + in (((fn_code f), (fn_entrypoint f)), pTreeEntry) |