From e836ec02384a11e2aa87567e828d69776dd453ee Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 17 Jan 2020 15:46:37 +0100 Subject: Removed unnecessary .mli file (provoked compilation problems) --- backend/DuplicateOpcodeHeuristic.mli | 12 ------------ 1 file changed, 12 deletions(-) delete mode 100644 backend/DuplicateOpcodeHeuristic.mli 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 -- cgit