From 9fc20c8cfbd258ffb113a1a14ffc16fb6b9c95a0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20Tj=C3=A4der?= <henrik@tjaders.com>
Date: Sun, 5 Mar 2017 22:40:18 +0100
Subject: [PATCH] Force KLEE to play within bounds and cleanup
---
include/SRP_wcet.h | 2 --
klee_stm_gdb.py | 2 +-
src/main.c | 11 +++++++----
3 files changed, 8 insertions(+), 7 deletions(-)
diff --git a/include/SRP_wcet.h b/include/SRP_wcet.h
index 609d5ef..8894583 100644
--- a/include/SRP_wcet.h
+++ b/include/SRP_wcet.h
@@ -66,5 +66,3 @@ locks eventlist[MAX_NUM_LOCKS];
#define BREAKPOINT
void finish_execution(void) {}
-//void terminate_execution(void) {}
-
diff --git a/klee_stm_gdb.py b/klee_stm_gdb.py
index f6ab1c5..d59e056 100644
--- a/klee_stm_gdb.py
+++ b/klee_stm_gdb.py
@@ -33,7 +33,7 @@ cur.execute('''CREATE TABLE IF NOT EXISTS events
FILE TEXT NOT NULL,
TIME INT NOT NULL,
RESOURCE TEXT NOT NULL,
- ACTION TEXT
+ ACTION TEXT,
JOB TEXT);''')
diff --git a/src/main.c b/src/main.c
index 83de52d..c2ccd95 100644
--- a/src/main.c
+++ b/src/main.c
@@ -44,9 +44,7 @@
// Analysis variables
static volatile int state;
-#ifdef KLEE
static int job;
-#endif
void work(int i) {
volatile int k = 0;
@@ -100,9 +98,13 @@ TASK(j3) {
int main() {
klee_make_symbolic(&job, sizeof(job), "job");
+ klee_assume(job > 0 && job < 4);
+
switch (job) {
- case 1:
+ default:
+ klee_make_symbolic(&state, sizeof(state), "state");
// check task 1
+ case 1:
klee_make_symbolic(&state, sizeof(state), "state");
EXTI1_IRQHandler();
break;
@@ -116,12 +118,13 @@ int main() {
klee_make_symbolic(&state, sizeof(state), "state");
EXTI3_IRQHandler();
break;
+ /*klee_make_symbolic(&state, sizeof(state), "state");*/
+ /*break;*/
}
}
#elif defined KLEE_WCET
/* The case when gdb runs WCET benchmarking */
-static int state;
static int job;
int main() {
--
GitLab