diff --git a/klee/tasks.txt b/klee/tasks.txt deleted file mode 100644 index 4427f9cd78222d49ef72dfaa961acb383408715c..0000000000000000000000000000000000000000 --- a/klee/tasks.txt +++ /dev/null @@ -1,2 +0,0 @@ -// autogenerated file -["EXTI2", "EXTI3", "EXTI1"] \ No newline at end of file diff --git a/klee_stm_gdb.py b/klee_stm_gdb.py index 4175eac81df1584a21b9f527eacb244ba4a5bce3..76defee40b7592e3cd17bfc62ea996ab93f2bc0f 100644 --- a/klee_stm_gdb.py +++ b/klee_stm_gdb.py @@ -128,8 +128,6 @@ def do_continue(): class MainBP(gdb.Breakpoint): def stop(self): - global file_index_current - global outputdata global init_done if self.location == "init": @@ -160,6 +158,7 @@ def stop_event(evt): global file_list cyccnt = gdb_cyccnt_read() + file_name = file_list[file_index_current].split('/')[-1] """ Get the current ceiling level, cast it to an integer """ @@ -167,22 +166,21 @@ def stop_event(evt): ceiling = int(gdb.parse_and_eval("ceiling"). cast(gdb.lookup_type('u8'))) except gdb.error: - # print("Returned from call to %s" % task_name) """ If there is no ceiling, it means we have returned to init since every claim have ceiling """ # gdb.events.stop.disconnect(stop_event) - outputdata.append([task_name, cyccnt, 0, "Finish"]) - - print("Claims:") - for x in outputdata: - print("%s" % x) + outputdata.append([file_name, task_name, cyccnt, 0, "Finish"]) if file_index_current < len(file_list) - 1: gather_data() else: + print("\nFinished all ktest files!\n") + print("Claims:") + for x in outputdata: + print("%s" % x) gdb.execute("quit") return @@ -201,7 +199,7 @@ def stop_event(evt): else: action = "Enter" - outputdata.append([task_name, cyccnt, ceiling, action]) + outputdata.append([file_name, task_name, cyccnt, ceiling, action]) """ Prepare a prompt for do_continue() @@ -243,6 +241,8 @@ def posted_event_init(): global task_to_test global task_name global file_index_current + global file_list + global outputdata """ Load the variable data """ ktest_setdata(file_index_current) @@ -253,17 +253,21 @@ def posted_event_init(): gdb_cyccnt_enable() gdb_cyccnt_reset() - print("Tasks: ", tasks) + # print("Tasks: ", tasks) # print("Name of task to test:", tasks[task_to_test]) if task_to_test > len(tasks): print("Nothing to call...") do_continue() return + if not task_to_test == -1: + task_name = tasks[task_to_test] + file_name = file_list[file_index_current].split('/')[-1] + outputdata.append([file_name, task_name, 0, 0, "Start"]) + gdb.write('Task to call: %s \n' % ( tasks[task_to_test] + "()")) - task_name = tasks[task_to_test] # gdb.prompt_hook = prompt gdb.execute('call %s' % "stub_" + tasks[task_to_test] + "()") @@ -285,7 +289,7 @@ def gather_data(): if file_index_current < len(file_list): init_done = 0 file_index_current += 1 - print("Current file: %s" % file_list[file_index_current]) + # print("Current file: %s" % file_list[file_index_current]) gdb.post_event(posted_event_init) else: @@ -564,7 +568,9 @@ file_list = ktest_iterate() """ Get all the tasks to jump to """ tasks = tasklist_get() -# print(tasks) +print("Available tasks:") +for t in tasks: + print(t) """ Run until the next breakpoint """ gdb.execute("c")