destructive_gen_data.py for python 3.5

destructive_gen_data.py

@@ -99,14 +99,14 @@ def parse_file(f):
 
 def compute_annots(FILES):
     total = {}
-    o = subprocess.check_output(["tokei", "--output=json", "--files"] + FILES)
+    o = subprocess.check_output(["tokei", "--output=json", "--files"] + FILES).decode("utf8")
     # print(o)
     inner = json.loads(o)
-    if "CHeader" not in inner:
-        inner["CHeader"] = { "code": 0, "reports": []}
-    lines_total = inner["C"]["code"] + inner["CHeader"]["code"]
+    if "C Header" not in inner:
+        inner["C Header"] = { "code": 0, "reports": []}
+    lines_total = inner["C"]["code"] + inner["C Header"]["code"]
     lines_per_file = {}
-    for s in inner["C"]["reports"] + inner["CHeader"]["reports"]:
+    for s in inner["C"]["reports"] + inner["C Header"]["reports"]:
         lines_per_file[s["name"]] = s["stats"]["code"]
 
     # count annotations
@@ -143,7 +143,7 @@ def compute_annots(FILES):
         shutil.copyfile(f, tmpname)
         with open(f, "a") as fd:
             fd.write("//@rc::import enable_debug from refinedc.typing.automation\n")
-            fd.write(f"//@rc::inlined Definition marker_{random.randint(0, 1000)} := tt.\n")
+            fd.write("//@rc::inlined Definition marker_{} := tt.\n".format(random.randint(0, 1000)))
 
         subprocess.check_output(["dune", "exec", "--", "refinedc", "check", "--no-build", f])
 
@@ -261,7 +261,16 @@ stats = [ {
 #   iAssert (spinlock_token γ []) with "[Hown]" as "?"; [ by iExists _; iFrame |].
 #   iModIntro.
 #   liInst Hevar γ.
-stats[5]["progs"][0]["stats"]["annot"] += 6
+for cat in stats:
+    for prog in cat["progs"]:
+        # set to 0 if missing
+        prog["stats"]["annot"] = prog["stats"].get("annot", 0)
+        prog["stats"]["pure"] = prog["stats"].get("pure", 0)
+
+        if prog["name"] == "Spinlock":
+            prog["stats"]["annot"] += 6
+        prog["stats"]["overhead"] = round((prog["stats"]["annot"] + prog["stats"]["pure"]) / prog["stats"]["LoC"], 1)
+
 
 # print(json.dumps(stats, indent=2))