1 /*
2  * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3  *
4  * SPDX-License-Identifier: BSD-2-Clause
5  */
6 
7 #pragma once
8 
9 #include <autoconf.h>
10 
11 /* Defined for each architecture: the number of hardware breakpoints
12  * available.
13  */
14 #ifdef CONFIG_HARDWARE_DEBUG_API
15 #define seL4_NumHWBreakpoints (4)
16 #define seL4_FirstBreakpoint (-1)
17 #define seL4_NumExclusiveBreakpoints (0)
18 #define seL4_FirstWatchpoint (-1)
19 #define seL4_NumExclusiveWatchpoints (0)
20 #define seL4_FirstDualFunctionMonitor (0)
21 #define seL4_NumDualFunctionMonitors (4)
22 #endif
23