Force KLEE to play within bounds and cleanup

include/SRP_wcet.h

@@ -66,5 +66,3 @@ locks eventlist[MAX_NUM_LOCKS];
 #define BREAKPOINT
 
 void finish_execution(void) {}
-//void terminate_execution(void) {}
-

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);''')
 
 

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() {