Autoformat main

src/main.c

@@ -46,21 +46,27 @@
 static volatile int state;
 static int job;
 
-void work(int i) {
+void work(int i)
+{
     volatile int k = 0;
-	for (int j = 0; j < 100 * i; j++) {
+    for (int j = 0; j < 100 * i; j++)
+    {
         k++;
     }
 }
 
-TASK(j1) {
+TASK(j1)
+{
     TRACE("j1_enter\n");
     LOCK(r2);
     JOB_REQUEST(j2); 			// job execution request for j2
 
-	if (state > 0) {
+    if (state > 0)
+    {
         work(10);
-	} else {
+    }
+    else
+    {
         work(5);
     }
 
@@ -73,7 +79,8 @@ TASK(j1) {
     UNLOCK(r2);
 }
 
-TASK(j2) {
+TASK(j2)
+{
     TRACE("j2_enter\n");
     LOCK(r1);
     TRACE("j2_r1_locked\n");
@@ -82,7 +89,8 @@ TASK(j2) {
     TRACE("j2_exit\n");
 }
 
-TASK(j3) {
+TASK(j3)
+{
     TRACE("j3_enter\n");
     LOCK(r1);
     TRACE("j3_r1_locked\n");
@@ -95,12 +103,14 @@ TASK(j3) {
 #ifdef KLEE
 /* The case when KLEE makes the path analysis */
 
-int main() {
+int main()
+{
     klee_make_symbolic(&job, sizeof(job), "job");
 
     klee_assume(job > 0 && job < 4);
 
-	switch (job) {
+    switch (job)
+    {
     default:
         klee_make_symbolic(&state, sizeof(state), "state");
     // check task 1
@@ -118,20 +128,20 @@ 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 job;
-int main() {
+int main()
+{
 
     dwt_enable();
     DWT->CYCCNT = 0;
 
-	switch (job) {
+    switch (job)
+    {
     case 1:
         TRACE_EVENT(S, j1);
         EXTI1_IRQHandler();
@@ -150,12 +160,12 @@ int main() {
     }
 
     finish_execution();			// gdb breakpoint
-	// terminate_execution();
 }
 
 #else
 // this will be run in the production code
-int main() {
+int main()
+{
     TRACE("\nInit\n");
     SETPRIO(j1);				// Set HW priorities
     SETPRIO(j2);