From 40e9fb8153a218a243cff749d7d0b4e82d70ae94 Mon Sep 17 00:00:00 2001
From: jaseg <git@jaseg.net>
Date: Mon, 17 Dec 2018 12:26:51 +0900
Subject: Invocation of noise.c from demo.c mostly proving in frama-c

---
 src/tracing.h | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/tracing.h')

diff --git a/src/tracing.h b/src/tracing.h
index 9aa9216..1970556 100644
--- a/src/tracing.h
+++ b/src/tracing.h
@@ -3,8 +3,13 @@
 
 #include <libopencm3/stm32/gpio.h>
 
+#ifndef VERIFICATION
 #define TRACING_SET(i) gpio_set(GPIOD, (1<<i))
 #define TRACING_CLEAR(i) gpio_clear(GPIOD, (1<<i))
+#else
+#define TRACING_SET(i) ((void)0)
+#define TRACING_CLEAR(i) ((void)0)
+#endif
 
 enum tracing_channels {
     TR_HID_MESSAGE_HANDLER = 0,
-- 
cgit