diff options
Diffstat (limited to 'backend/DuplicateOpcodeHeuristic.mli')
| -rw-r--r-- | backend/DuplicateOpcodeHeuristic.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/DuplicateOpcodeHeuristic.mli b/backend/DuplicateOpcodeHeuristic.mli index a4cc4848..b4c9f1ef 100644 --- a/backend/DuplicateOpcodeHeuristic.mli +++ b/backend/DuplicateOpcodeHeuristic.mli @@ -3,6 +3,8 @@ * 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, |