slowbeast: generate a trivial correctness witness

staticafi · Dec 16, 2020 · 7134bcf · 7134bcf
1 parent 6ebf9db
commit 7134bcf
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/lib/symbioticpy/symbiotic/targets/slowbeast.py b/lib/symbioticpy/symbiotic/targets/slowbeast.py
@@ -78,6 +78,17 @@ def passes_before_verification(self):
             passes.append(",".join(prp.getcalls())+f",__VERIFIER_assert")
         return passes + ["-O3", "-remove-constant-exprs", "-reg2mem"]
 
+    def generate_graphml(path, source, is_correctness_wit, opts, saveto):
+        """ Generate trivial correctness witness for now """
+        if saveto is None:
+            saveto = '{0}.graphml'.format(basename(path))
+            saveto = abspath(saveto)
+
+        if is_correctness_wit:
+            gen.createTrivialWitness()
+            assert path is None
+        gen.write(saveto)
+
     def determine_result(self, returncode, returnsignal, output, isTimeout):
         if isTimeout:
             return ''