Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Helper changes for symbolic testing #769

Merged
merged 38 commits into from
May 12, 2020
Merged

Helper changes for symbolic testing #769

merged 38 commits into from
May 12, 2020

Conversation

denis-bogdanas
Copy link
Contributor

No description provided.

edsl.md Outdated Show resolved Hide resolved
edsl.md Outdated Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
serialization.md Outdated Show resolved Hide resolved
evm-types.md Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
tests/specs/lemmas.k Outdated Show resolved Hide resolved
tests/specs/lemmas.k Outdated Show resolved Hide resolved
tests/specs/lemmas.k Outdated Show resolved Hide resolved
@denis-bogdanas
Copy link
Contributor Author

@ehildenb Except one question above this is ready for review. Should pass the tests.

tests/specs/lemmas.k Outdated Show resolved Hide resolved
@ehildenb
Copy link
Member

ehildenb commented Apr 4, 2020

It looks pretty good to me, but can @daejunpark look and @virgil-serbanuta as well?

Copy link
Contributor

@virgil-serbanuta virgil-serbanuta left a comment

Choose a reason for hiding this comment

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

This seems reasonable, I have one small question.

evm-types.md Outdated Show resolved Hide resolved
edsl.md Outdated Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
@denis-bogdanas
Copy link
Contributor Author

@ehildenb @daejunpark All comments addressed. I see it passes now. No idea why it was failing before. Changes are unrelated to failure. Ready for re-review.

evm-types.md Outdated Show resolved Hide resolved
@ehildenb
Copy link
Member

Please don't merge the update submodule PR into this one @denis-bogdanas . Instead, you can just approve that PR and get it merged directly, then merge master into this one.

If other PRs update the submodules, then the submodule updater gets confused, it can't handle merge conflicts at all.

@denis-bogdanas
Copy link
Contributor Author

This PR would pass tests with latest K, but K update PR fails for other reasons as you can see. That one must be fixed first.

Copy link
Contributor

@virgil-serbanuta virgil-serbanuta left a comment

Choose a reason for hiding this comment

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

I still think that it would be better to ask the backend to resolve that ceil, but I guess that this is also fine.

@denis-bogdanas
Copy link
Contributor Author

@ehildenb We need updated K for this PR to pass. Other than that it looks ready.

@ehildenb
Copy link
Member

We're waiting on a regression in the LLVM backend to update K. I'll keep you posted, thanks!

evm-types.md Outdated Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
@denis-bogdanas
Copy link
Contributor Author

@ehildenb ready for review

evm-types.md Outdated Show resolved Hide resolved
evm.md Outdated Show resolved Hide resolved
evm-types.md Outdated Show resolved Hide resolved
@ehildenb ehildenb self-requested a review May 12, 2020 10:43
@ehildenb ehildenb merged commit 309d449 into master May 12, 2020
@ehildenb ehildenb deleted the symb-test-prep branch May 12, 2020 11:29
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.

4 participants