diff --git a/Makefile b/Makefile index db988736bc320e255498974bbc74b01dcfac4613..7e5433de303ed81c2bda6419e8cbe852526f8914 100644 --- a/Makefile +++ b/Makefile @@ -50,7 +50,7 @@ DEFS = -DSTM32F40XX -DHSE_VALUE=8000000 -DTRACE -DOS_USE_TRACE_ITM else ifeq "$(MAKECMDGOALS)" "wcet" DEFS = -DSTM32F40XX -DHSE_VALUE=8000000 -DTRACE -DOS_USE_TRACE_ITM -DKLEE_WCET else -DEFS = -DSTM32F40XX -DHSE_VALUE=8000000 -DKLEE +DEFS = -DSTM32F40XX -DHSE_VALUE=8000000 -DKLEE endif # Definitions diff --git a/klee_stm_gdb.py b/klee_stm_gdb.py index 14fe4cfc08fbd25b1e9a828a3e91c48b6acb43c5..f6ab1c52fd10cc7a74daad53f9ecd3a3bcdb822d 100644 --- a/klee_stm_gdb.py +++ b/klee_stm_gdb.py @@ -13,9 +13,6 @@ file_list = [] file_index_current = 0 object_index_current = 0 -""" For running different programs during WCET-benchmarking """ -wcet_task = 1 - """ Max number of events guard """ object_index_max = 100 @@ -182,6 +179,10 @@ def posted_event_finish_execution(): str(object_index_current) + "].action") + """ Parse which running job is active """ + + event_job = gdb.parse_and_eval("job") + """ print("file: %r " % str(file_list[file_index_current])) print("time: %r " % int(event_time)) @@ -195,7 +196,7 @@ def posted_event_finish_execution(): event.append(int(event_time)) event.append(str(event_resource)) event.append(str(event_action)) - event.append(str(wcet_task)) + event.append("j" + str(event_job)) print("Event: %r " % event)