From 9393daa283be63849dd518f697562c10808ea584 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20Tj=C3=A4der?= <henrik@tjaders.com>
Date: Sun, 5 Mar 2017 21:50:56 +0100
Subject: [PATCH] Small bugfixes
---
src/main.c | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/main.c b/src/main.c
index 5769321..83de52d 100644
--- a/src/main.c
+++ b/src/main.c
@@ -42,6 +42,12 @@
#define r1_Ceiling 2
#define r2_Ceiling 1
+// Analysis variables
+static volatile int state;
+#ifdef KLEE
+static int job;
+#endif
+
void work(int i) {
volatile int k = 0;
for (int j = 0; j < 100 * i; j++) {
@@ -90,8 +96,6 @@ TASK(j3) {
#ifdef KLEE
/* The case when KLEE makes the path analysis */
-static int state;
-static int job;
int main() {
klee_make_symbolic(&job, sizeof(job), "job");
@@ -113,6 +117,7 @@ int main() {
EXTI3_IRQHandler();
break;
}
+}
#elif defined KLEE_WCET
/* The case when gdb runs WCET benchmarking */
--
GitLab