/* SPDX-License-Identifier: GPL-2.0-only */ #include <types.h> void dummy_timestamp_set(uint64_t v); void dummy_timestamp_tick_freq_mhz_set(int v);