Skip to content

Commit

Permalink
Update dependency: deps/llvm-backend_release (#4648)
Browse files Browse the repository at this point in the history 
Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Theodoros Kasampalis <kasampalis.theodoros@gmail.com>
  • Loading branch information
@rv-jenkins @theo25
3 people authored Sep 25, 2024
1 parent 315cf79 commit 449726d
Show file tree
Hide file tree
Showing 8 changed files with 32 additions and 38 deletions.
2 changes: 1 addition & 1 deletion deps/llvm-backend_release
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.94
0.1.95
8 changes: 4 additions & 4 deletions flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion flake.nix
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
{
description = "K Framework";
inputs = {
llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.94";
llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.95";
haskell-backend = {
url = "github:runtimeverification/haskell-backend/v0.1.76";
inputs.rv-utils.follows = "llvm-backend/rv-utils";
Expand Down
Binary file modified k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out
View file
Binary file not shown.
Binary file modified k-distribution/tests/regression-new/proof-instrumentation/input.test.out
View file
Binary file not shown.
2 changes: 1 addition & 1 deletion llvm-backend/src/main/native/llvm-backend
Submodule llvm-backend updated 106 files
46 changes: 23 additions & 23 deletions pyk/src/tests/integration/kllvm/test_prooftrace.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,7 +103,7 @@ def test_streaming_parser_iter(self, header: prooftrace.KoreHeader, hints_file:
list_of_events = list(it)

# Test length of the list
assert len(list_of_events) == 14
assert len(list_of_events) == 13

# Test the type of the events
for event in list_of_events:
Expand Down Expand Up @@ -189,8 +189,8 @@ def test_parse_proof_hint_single_rewrite(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 2 post-initial-configuration events
assert len(pt.trace) == 2
Expand Down Expand Up @@ -259,8 +259,8 @@ def test_parse_proof_hint_reverse_no_ints(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 9 post-initial-configuration events
assert len(pt.trace) == 9
Expand Down Expand Up @@ -384,8 +384,8 @@ def test_parse_proof_hint_non_rec_function(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 6 post-initial-configuration events
assert len(pt.trace) == 6
Expand Down Expand Up @@ -467,8 +467,8 @@ def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader,
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 3 post-initial-configuration events
assert len(pt.trace) == 3
Expand Down Expand Up @@ -548,8 +548,8 @@ def test_parse_concurrent_counters(self, hints: bytes, header: prooftrace.KoreHe
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 37 post-initial-configuration events
assert len(pt.trace) == 37
Expand Down Expand Up @@ -708,8 +708,8 @@ def test_parse_proof_hint_0_decrement(self, hints: bytes, header: prooftrace.Kor
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 1 post-initial-configuration event
assert len(pt.trace) == 1
Expand Down Expand Up @@ -737,8 +737,8 @@ def test_parse_proof_hint_1_decrement(self, hints: bytes, header: prooftrace.Kor
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 2 post-initial-configuration events
assert len(pt.trace) == 2
Expand Down Expand Up @@ -766,8 +766,8 @@ def test_parse_proof_hint_2_decrement(self, hints: bytes, header: prooftrace.Kor
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 3 post-initial-configuration events
assert len(pt.trace) == 3
Expand Down Expand Up @@ -805,8 +805,8 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 776 post-initial-configuration events
assert len(pt.trace) == 776
Expand Down Expand Up @@ -914,8 +914,8 @@ def test_parse_proof_hint_imp5(self, hints: bytes, header: prooftrace.KoreHeader
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 16 initialization events
assert len(pt.pre_trace) == 16
# 14 initialization events
assert len(pt.pre_trace) == 14

# 2 post-initial-configuration events
assert len(pt.trace) == 2
Expand Down Expand Up @@ -953,8 +953,8 @@ def test_parse_proof_hint_builtin_hook_events(
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 4 post-initial-configuration events
assert len(pt.trace) == 4
Expand Down
10 changes: 2 additions & 8 deletions pyk/src/tests/integration/test_krun_proof_hints.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,6 @@ class Test0Decrement(KRunTest, ProofTraceTest):
"""

HINTS_OUTPUT = """version: 13
hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
arg: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
hook: MAP.unit Lbl'Stop'Map{} ()
hook result: kore[Lbl'Stop'Map{}()]
hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
arg: kore[Lbl'Stop'Map{}()]
arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
Expand Down Expand Up @@ -73,8 +67,8 @@ def test_parse_proof_hint_0_decrement(self, krun: KRun, header: prooftrace.KoreH
pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
assert pt is not None

# 12 initialization events
assert len(pt.pre_trace) == 12
# 10 initialization events
assert len(pt.pre_trace) == 10

# 1 post-initial-configuration event
assert len(pt.trace) == 1
Expand Down

0 comments on commit 449726d

Please sign in to comment.