fix tests

runtimeverification · May 13, 2024 · 1a82545 · 1a82545
1 parent 62e83cc
commit 1a82545
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/test/python/test_proof_trace.py b/test/python/test_proof_trace.py
@@ -3,6 +3,7 @@
 # RUN: export IN=$(realpath Inputs/proof-trace.in)
 # RUN: cd %t && %kompile "$KORE_DEF" main --proof-hint-instrumentation -o interpreter
 # RUN: rm -f proof_trace.bin && ./interpreter "$IN" -1 proof_trace.bin --proof-output
+# RUN: kore-rich-header "$KORE_DEF" > %t/header.bin
 
 
 # RUN: %python %s
@@ -19,9 +20,13 @@ def test_file(self):
         binary_proof_trace = os.path.join(
             os.path.dirname(os.path.realpath(__file__)),
             "Output", "test_proof_trace.py.tmp", "proof_trace.bin")
+        binary_header_path = os.path.join(
+            os.path.dirname(os.path.realpath(__file__)),
+            "Output", "test_proof_trace.py.tmp", "header.bin")
+        header = kllvm.prooftrace.kore_header(binary_header_path)
         with open(binary_proof_trace, 'rb') as f:
            data = f.read()
-           trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data)
+           trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data, header)
            self.assertFalse(trace is None)
 
            # check that there is a initial configuration

diff --git a/test/python/test_proof_trace_slow.py b/test/python/test_proof_trace_slow.py
@@ -3,6 +3,7 @@
 # RUN: export IN=$(realpath Inputs/proof-trace.in)
 # RUN: cd %t && %kompile "$KORE_DEF" main --proof-hint-instrumentation-slow -o interpreter
 # RUN: rm -f proof_trace.bin && ./interpreter "$IN" -1 proof_trace.bin --proof-output
+# RUN: kore-rich-header "$KORE_DEF" > %t/header.bin
 
 
 # RUN: %python %s
@@ -19,9 +20,13 @@ def test_file(self):
         binary_proof_trace = os.path.join(
             os.path.dirname(os.path.realpath(__file__)),
             "Output", "test_proof_trace_slow.py.tmp", "proof_trace.bin")
+        binary_header_path = os.path.join(
+            os.path.dirname(os.path.realpath(__file__)),
+            "Output", "test_proof_trace_slow.py.tmp", "header.bin")
+        header = kllvm.prooftrace.kore_header(binary_header_path)
         with open(binary_proof_trace, 'rb') as f:
            data = f.read()
-           trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data)
+           trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data, header)
            self.assertFalse(trace is None)
 
            # check that there is a initial configuration