| /* |
| * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) |
| * |
| * SPDX-License-Identifier: BSD-2-Clause |
| */ |
| #pragma once |
| |
| #include <sel4test/test.h> |
| #include "test.h" |
| #include <sel4testsupport/testreporter.h> |
| |
| #define TIMER_ID 0 |
| |
| /* Timing related functions used only by in sel4test-driver */ |
| void handle_timer_interrupts(driver_env_t env, seL4_Word badge); |
| void wait_for_timer_interrupt(driver_env_t env); |
| void timeout(driver_env_t env, uint64_t ns, timeout_type_t timeout); |
| uint64_t timestamp(driver_env_t env); |
| void timer_reset(driver_env_t env); |
| void timer_cleanup(driver_env_t env); |
