Fixed the macro and formatted main

include/SRP_wcet.h

@@ -44,14 +44,15 @@ typedef struct locks
 
 } locks;
 
-uint32_t event_count = 0;
 
-#define MAX_NUM_LOCKS 10
+
+int event_count = 0;
 
 /* Create array containing structs of type locks */
+#define MAX_NUM_LOCKS 10
 locks eventlist[MAX_NUM_LOCKS];
-//#define TRACE_EVENT(event, el)({eventlist[event_count].time = DWT->CYCCNT; eventlist[event_count].action = event; eventlist[event_count].elem = el; event_count+=1;})
-#define TRACE_EVENT(event, el)({})
+
+#define TRACE_EVENT(event, el)({eventlist[event_count].time = DWT->CYCCNT; eventlist[event_count].action = event; eventlist[event_count].elem = el; event_count+=1;})
 
 
 // #define Ceiling(R)		(R##_Ceiling)
@@ -64,8 +65,8 @@ locks eventlist[MAX_NUM_LOCKS];
 // #define BARRIER_UNLOCK 	{ }
 #define JOB_REQUEST(J)	{ }
 
-#define LOCK(R) 		TRACE_EVENT(L, #R);
-#define UNLOCK(R) 		TRACE_EVENT(R, #R);
+#define LOCK(X) 		TRACE_EVENT(L, X);
+#define UNLOCK(X) 		TRACE_EVENT(R, X);
 
 // #define SETPRIO(J)		{ }
 // #define ENABLE(J)		{ }

src/main.c

@@ -31,23 +31,30 @@
 
 static int state;
 
-void work(int i) {
+void work(int i)
+{
     volatile int k =0;
     for (int j =0; j < 100 * i; j++)
+    {
         k++;
     }
+}
 
-TASK(j1) {
+TASK(j1)
+{
     LOCK(r2);
 
     JOB_REQUEST(j2); 			// job execution request for j2
 
     if (state > 0)
+    {
         work(10);
+    }
     else
+    {
         work(5);
+    }
 
-		/*
     LOCK(r1);
 #ifdef enable_itm
     trace_printf("j1_r1_locked, before job request j2\n");
@@ -57,11 +64,11 @@ TASK(j1) {
     trace_printf("j1_r1_locked, after job request j2\n");
 #endif
     UNLOCK(r1);
-		*/
     UNLOCK(r2);
 }
 
-TASK(j2) {
+TASK(j2)
+{
 #ifdef enable_itm
     trace_printf("j2_enter\n");
 #endif
@@ -75,14 +82,18 @@ TASK(j2) {
 #endif
 }
 
-int main() {
+int main()
+{
 #ifdef enable_itm
     trace_printf("\nInit\n");
 #endif
 
 #ifndef KLEE
 
+    dwt_enable();
+    DWT->CYCCNT = 0;
 #ifndef KLEE_WCET
+
     SETPRIO(j1);				// Set HW priorities
     SETPRIO(j2);
     SETPRIO(j3);
@@ -96,17 +107,17 @@ int main() {
     BREAKPOINT;
     while (1) ;
     return 0;
+
+    /* The case when NOT running WCET benchmark nor KLEE-analysis */
 #else
-	dwt_enable();
-	DWT->CYCCNT = 0;
 
-	event_count = 0;
     TRACE_EVENT(S, j1);
     EXTI1_IRQHandler();
     TRACE_EVENT(E, j1);
+#endif
+
     finish_execution();
     terminate_execution();
-	#endif
 
 #elif (JOB == 1)
     // check task 1