Skip to content

Conversation

@andreiburdusa
Copy link
Contributor

@andreiburdusa andreiburdusa commented Dec 2, 2021

Fixes #2879

Scope: Use matching in Kore.Rewrite.Search.matchWith

Estimate: December, 2


Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

  • Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
  • Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
  • Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
  • Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

@github-actions
Copy link

github-actions bot commented Dec 2, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-pop1.sh -0.000000 -0.022412
test/regression-evm/test-branching-invalid.sh 0.000453 0.092724
test/regression-evm/test-straight-line-no-invalid.sh 0.000629 -0.000000
test/regression-evm/test-addu48u48.sh 0.000000 -0.000000
test/regression-evm/test-storagevar03.sh -0.000002 0.002531
test/regression-evm/test-add0.sh -0.000000 -0.064668
test/regression-evm/test-lemmas.sh -0.000005 -0.004412
test/regression-evm/test-straight-line.sh 0.000546 -0.022699
test/regression-evm/test-sumTo10.sh 0.000000 -0.003255
test/regression-evm/test-totalSupply.sh -0.000000 0.000000
test/regression-evm/test-and0.sh 0.000000 -0.000000
test/regression-evm/test-branching-no-invalid.sh 0.000572 0.014436
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.000004 -0.128904
test/regression-evm/test-sha3_bigSize.sh -0.000000 -0.000003
test/regression-evm/test-mul0.sh 0 -0.017467
test/regression-evm/test-sum-to-n.sh 0.000001 0
test/regression-wasm/test-memory.sh -0.000000 0
test/regression-wasm/test-locals.sh 0.000001 -0.000001
test/regression-wasm/test-wrc20.sh 0.000009 -0.005172
test/regression-wasm/test-simple-arithmetic.sh -0.000009 0.000067
test/regression-wasm/test-loops.sh 0.000002 0.000001

@andreiburdusa andreiburdusa marked this pull request as ready for review December 2, 2021 13:42
@ana-pantilie ana-pantilie self-requested a review December 2, 2021 15:14
Copy link
Contributor

@ana-pantilie ana-pantilie left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just had a small comment.

, Conditional.predicate e2
]
[Conditional.substitution predSubst]
[from substitution]
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add a type annotation here to indicate the type transformation.

@github-actions
Copy link

github-actions bot commented Dec 6, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-pop1.sh -0.000000 0.000000
test/regression-evm/test-branching-invalid.sh 0.000454 0.032870
test/regression-evm/test-straight-line-no-invalid.sh 0.000629 -0.000000
test/regression-evm/test-addu48u48.sh 0.000002 -0.000000
test/regression-evm/test-storagevar03.sh 0.000000 0.000357
test/regression-evm/test-add0.sh 0.000000 0.010446
test/regression-evm/test-lemmas.sh 0.000018 0
test/regression-evm/test-straight-line.sh 0.000547 -0.000001
test/regression-evm/test-sumTo10.sh 0.000000 -0.003243
test/regression-evm/test-totalSupply.sh 0.000000 0.000000
test/regression-evm/test-and0.sh -0.000000 -0.000001
test/regression-evm/test-branching-no-invalid.sh 0.000572 -0.040620
test/regression-evm/test-dsvalue-peek-pass-rough.sh 0.000009 -0.113106
test/regression-evm/test-sha3_bigSize.sh 0.000000 -0.003208
test/regression-evm/test-mul0.sh 0.000000 -0.000001
test/regression-evm/test-sum-to-n.sh -0.000003 0
test/regression-wasm/test-memory.sh -0.000009 -0.000001
test/regression-wasm/test-locals.sh -0.000000 0.000000
test/regression-wasm/test-wrc20.sh -0.000007 -0.001276
test/regression-wasm/test-simple-arithmetic.sh -0.000018 0.000001
test/regression-wasm/test-loops.sh 0.000003 0

@github-actions
Copy link

github-actions bot commented Dec 6, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-pop1.sh -0.000000 -0.000000
test/regression-evm/test-branching-invalid.sh 0.000454 -0.005445
test/regression-evm/test-straight-line-no-invalid.sh 0.000629 -0.000000
test/regression-evm/test-addu48u48.sh 0.000000 -0.083407
test/regression-evm/test-storagevar03.sh -0.000009 -0.000822
test/regression-evm/test-add0.sh -0.000000 -0.000000
test/regression-evm/test-lemmas.sh -0.000009 0.004141
test/regression-evm/test-straight-line.sh 0.000547 -0.005145
test/regression-evm/test-sumTo10.sh 0.000001 0.002407
test/regression-evm/test-totalSupply.sh 0.000001 -0.000000
test/regression-evm/test-and0.sh 0.000000 0.038062
test/regression-evm/test-branching-no-invalid.sh 0.000572 -0.031550
test/regression-evm/test-dsvalue-peek-pass-rough.sh 0.000003 0.004651
test/regression-evm/test-sha3_bigSize.sh -0.000000 0.003220
test/regression-evm/test-mul0.sh 0.000000 0.038061
test/regression-evm/test-sum-to-n.sh -0.000000 0.011101
test/regression-wasm/test-memory.sh 0.000003 -0.000000
test/regression-wasm/test-locals.sh 0 0
test/regression-wasm/test-wrc20.sh 0.000008 0.001231
test/regression-wasm/test-simple-arithmetic.sh 0.000003 0.000001
test/regression-wasm/test-loops.sh 0.000026 -0.000314

@rv-jenkins rv-jenkins merged commit dd3d4d9 into master Dec 6, 2021
@rv-jenkins rv-jenkins deleted the issue-2879-unification-matching branch December 6, 2021 11:10
@github-actions
Copy link

github-actions bot commented Dec 6, 2021

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-pop1.sh -0.000000 0.000001
test/regression-evm/test-branching-invalid.sh 0.000000 0.066253
test/regression-evm/test-straight-line-no-invalid.sh -0.000000 -0.000000
test/regression-evm/test-addu48u48.sh -0.000000 0.089251
test/regression-evm/test-storagevar03.sh -0.000023 -0.002402
test/regression-evm/test-add0.sh -0.000000 -0.048562
test/regression-evm/test-lemmas.sh -0.000016 0.016472
test/regression-evm/test-straight-line.sh 0.000000 -0.010687
test/regression-evm/test-sumTo10.sh 0.000000 0.023264
test/regression-evm/test-totalSupply.sh -0.000007 -0.107282
test/regression-evm/test-and0.sh 0 0.021687
test/regression-evm/test-branching-no-invalid.sh -0.000000 -0.004910
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.000007 -0.103677
test/regression-evm/test-sha3_bigSize.sh 0.000000 0.000002
test/regression-evm/test-mul0.sh 0.000000 0.088401
test/regression-evm/test-sum-to-n.sh 0.000012 0
test/regression-wasm/test-memory.sh -0.000003 0
test/regression-wasm/test-locals.sh 0.000000 0
test/regression-wasm/test-wrc20.sh 0.000004 -0.002110
test/regression-wasm/test-simple-arithmetic.sh 0.000003 -0.000001
test/regression-wasm/test-loops.sh 0.000027 0

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Bug: kore-match-disjunction returns \bottom when it should not

4 participants