Introduced JOB-field to database and removed terminate_execution

klee_stm_gdb.py

@@ -13,8 +13,11 @@ 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 = 10
+object_index_max = 100
 
 database_name = "klee_profiling"
 
@@ -33,7 +36,8 @@ 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);''')
 
 
 class KTestError(Exception):
@@ -191,14 +195,15 @@ 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))
 
         print("Event: %r " % event)
 
         try:
             cur = conn.cursor()
 
-            cur.execute('INSERT INTO events(FILE, TIME, RESOURCE, ACTION)\
-                        VALUES (?,?,?,?)', event)
+            cur.execute('INSERT INTO events(FILE, TIME, RESOURCE, ACTION, JOB)\
+                        VALUES (?,?,?,?,?)', event)
 
         except sqlite3.Error as e:
             print("An error occurred:", e.args[0])
@@ -280,6 +285,7 @@ def ktest_iterate():
 # AddBreakpoint("main")
 MainBP("main")
 
+
 """ Tell gdb-dashboard to hide """
 gdb.execute("dashboard -enabled off")
 gdb.execute("dashboard -output /dev/null")
@@ -287,7 +293,7 @@ gdb.execute("dashboard -output /dev/null")
 """ Also break at the main-loop """
 # AddBreakpoint("finish_execution")
 MainBP("finish_execution")
-MainBP("terminate_execution")
+# MainBP("terminate_execution")
 
 """Used for making it scriptable"""
 gdb.execute("set confirm off")

profiling_db_parser.py

@@ -145,6 +145,11 @@ def print_db_ktest():
                   (filename,))
         resources = c.fetchall()
 
+        c.execute('SELECT DISTINCT job FROM events WHERE (file=?)',
+                  (filename,))
+        job = c.fetchall()
+        print("Job: j%s" % job)
+
         """ Go through the unique list of resources
 
             If they are called multiple times this is handled later