diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-17 15:46:37 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-17 15:46:37 +0100 |
| commit | e836ec02384a11e2aa87567e828d69776dd453ee (patch) | |
| tree | b1ec17f59419b883d738807814cd5be4c0f2e947 | |
| parent | 675b6539607f387d43b8d7e04de31292b4246a1b (diff) | |
| download | compcert-kvx-e836ec02384a11e2aa87567e828d69776dd453ee.tar.gz compcert-kvx-e836ec02384a11e2aa87567e828d69776dd453ee.zip | |
Removed unnecessary .mli file (provoked compilation problems)
| -rw-r--r-- | backend/DuplicateOpcodeHeuristic.mli | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/backend/DuplicateOpcodeHeuristic.mli b/backend/DuplicateOpcodeHeuristic.mli deleted file mode 100644 index b4c9f1ef..00000000 --- a/backend/DuplicateOpcodeHeuristic.mli +++ /dev/null @@ -1,12 +0,0 @@ -(** Define opcode heuristics used for the instruction duplication oracle - * In particular, it is used to figure out which "branch" should be privileged - * when selecting a trace. - *) - -exception HeuristicSucceeded - -(* The bool reference should be updated to [true] if the condition is supposed - * to hold, [false] if it is supposed to not hold - * The function should raise HeuristicSucceeded if it succeeded to predict a branch, - * and do nothing otherwise *) -val opcode_heuristic : RTL.code -> Op.condition -> RTL.node -> RTL.node -> bool ref -> unit |