From 3017f9b72aab4061ef9ab9007e9d4c6e7d0adc42 Mon Sep 17 00:00:00 2001
From: Anna Lyons <Anna.Lyons@data61.csiro.au>
Date: Thu, 23 Nov 2017 15:41:13 +1100
Subject: [PATCH] Move timestamp_t definition to types.h

it was causing circular references in files where it is defined and
hardware macros are also used.
---
 include/arch/arm/arch/32/mode/types.h             | 2 ++
 include/arch/arm/arch/benchmark.h                 | 2 --
 include/arch/arm/arch/benchmark_overflowHandler.h | 1 +
 include/arch/x86/arch/benchmark.h                 | 2 --
 include/arch/x86/arch/types.h                     | 2 ++
 include/benchmark/benchmark_utilisation_.h        | 2 +-
 6 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/include/arch/arm/arch/32/mode/types.h b/include/arch/arm/arch/32/mode/types.h
index 8d11b1b4d..414b30043 100644
--- a/include/arch/arm/arch/32/mode/types.h
+++ b/include/arch/arm/arch/32/mode/types.h
@@ -16,4 +16,6 @@
 #define wordRadix 5
 #define wordBits (1 << wordRadix)
 
+typedef uint32_t timestamp_t;
+
 #endif /* __ARCH_MODE_TYPES_H_ */
diff --git a/include/arch/arm/arch/benchmark.h b/include/arch/arm/arch/benchmark.h
index 2ff52a640..af49a87b6 100644
--- a/include/arch/arm/arch/benchmark.h
+++ b/include/arch/arm/arch/benchmark.h
@@ -16,8 +16,6 @@
 
 #include <armv/benchmark.h>
 
-typedef uint32_t timestamp_t;
-
 void armv_init_ccnt(void);
 
 #endif /* CONFIG_ENABLE_BENCHMARKS */
diff --git a/include/arch/arm/arch/benchmark_overflowHandler.h b/include/arch/arm/arch/benchmark_overflowHandler.h
index 0137faad5..193796d5d 100644
--- a/include/arch/arm/arch/benchmark_overflowHandler.h
+++ b/include/arch/arm/arch/benchmark_overflowHandler.h
@@ -17,6 +17,7 @@
 
 #ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
 #include <model/statedata.h>
+#include <armv/benchmark.h>
 #include <armv/benchmark_irqHandler.h>
 
 extern bool_t benchmark_log_utilisation_enabled;
diff --git a/include/arch/x86/arch/benchmark.h b/include/arch/x86/arch/benchmark.h
index e68556c53..49ec792c6 100644
--- a/include/arch/x86/arch/benchmark.h
+++ b/include/arch/x86/arch/benchmark.h
@@ -14,8 +14,6 @@
 #include <config.h>
 #ifdef CONFIG_ENABLE_BENCHMARKS
 
-typedef uint64_t timestamp_t;
-
 static inline uint64_t
 timestamp(void)
 {
diff --git a/include/arch/x86/arch/types.h b/include/arch/x86/arch/types.h
index ff8b711f1..308cb4424 100644
--- a/include/arch/x86/arch/types.h
+++ b/include/arch/x86/arch/types.h
@@ -42,4 +42,6 @@ typedef uint8_t seL4_Uint8;
 typedef node_id_t seL4_NodeId;
 typedef paddr_t seL4_PAddr;
 typedef dom_t seL4_Domain;
+
+typedef uint64_t timestamp_t;
 #endif
diff --git a/include/benchmark/benchmark_utilisation_.h b/include/benchmark/benchmark_utilisation_.h
index bf4c49d87..73c6f5b07 100644
--- a/include/benchmark/benchmark_utilisation_.h
+++ b/include/benchmark/benchmark_utilisation_.h
@@ -14,7 +14,7 @@
 #define _BENCHMARK_UTILISATION_H
 
 #include <config.h>
-#include <arch/benchmark.h>
+#include <basic_types.h>
 
 #ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
 typedef struct {