cleanup

Author: lou1306

sliver/analysis/value_analysis.py

@@ -351,8 +351,8 @@ def parallel_merge(states):
             st_list = list(states)
             mid = len(st_list) // 2
             with ThreadPoolExecutor() as exc:
-                rec_left = exc.submit(parallelMerge, st_list[:mid])
-                rec_right = exc.submit(parallelMerge, st_list[mid:])
+                rec_left = exc.submit(parallel_merge, st_list[:mid])
+                rec_right = exc.submit(parallel_merge, st_list[mid:])
                 return mergeStates(rec_left.result(), rec_right.result())
 
     def loop(bound, guard_map, s0):

sliver/app/info.py

@@ -217,7 +217,7 @@ def items(self):
     def parse(c, picks=""):
         result = {}
         picks = dict([x.split(" ", 1) for x in picks.split(";")])
-        picks = {k: v.split("),(") for k,v in picks.items()}
+        picks = {k: v.split("),(") for k, v in picks.items()}
         reg = re.compile(r'\(+([^,]+),')
         for k in picks:
             matches = [reg.match(x) for x in picks[k] if reg.match(x)]
@@ -226,7 +226,7 @@ def parse(c, picks=""):
         for comp, iface, lstig in zip(c[::3], c[1::3], c[2::3]):
             name, rng = comp.split(" ")
             compmin, compmax = rng.split(",")
-            result[(int(compmin), int(compmax))] = Agent(name, iface, lstig, picks[name])
+            result[(int(compmin), int(compmax))] = Agent(name, iface, lstig, picks[name])  # noqa: E501
 
         return Spawn(result)
 

sliver/backends/esbmc.py

@@ -68,7 +68,7 @@ def preprocess(self, code, _):
         self.verbose_output(
             f"Value analysis: {ranges=}, {fix=}, {depends=}, {wont_change=}")
 
-        s_analysis, s_fix, *_  = value_analysis(self.cli, info, Sign)
+        s_analysis, s_fix, *_ = value_analysis(self.cli, info, Sign)
         self.verbose_output(f"Sign analysis: {s_analysis=}, {s_fix=}")
 
         rename = {"i": "I", "e": "E", "l": "Lvalue"}
@@ -180,21 +180,20 @@ def fmt_one(index):
                         continue
                     loop_assumptions.extend((
                         f"__CPROVER_assume({x});"
-                        for x in fmt_sign(var, sign, tid)))  # noqa: E501
+                        for x in fmt_sign(var, sign, tid)))
                 except KeyError:
                     # Local variable
                     continue
 
         loop_assumptions = "\n    ".join(loop_assumptions)
-        loop_assumptions = f"void __invariants(void) {{\n{loop_assumptions}\n}}"
+        loop_assumptions = f"void __invariants(void) {{\n{loop_assumptions}\n}}"  # noqa: E501
         code = code.replace(
             """void __invariants(void) { }""",
             loop_assumptions)
 
         head_of_loop = re.compile(r'while\s*\(1\)\s*{')
         code = head_of_loop.sub("while (1) {\n __invariants();", code)
 
-
         esbmc_conf = """
         (without-bitwise)
         (replace-calls