Skip to content

.gitignore update: rust source dir #587

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

Merged
merged 3 commits into from
Jul 2, 2019
Merged

.gitignore update: rust source dir #587

merged 3 commits into from
Jul 2, 2019

Conversation

denis-bogdanas
Copy link
Contributor

No description provided.

@denis-bogdanas denis-bogdanas requested a review from ehildenb July 2, 2019 17:37
@ehildenb ehildenb merged commit bf16bc2 into master Jul 2, 2019
@ehildenb ehildenb deleted the gitignore-upd branch July 2, 2019 22:05
rv-jenkins added a commit that referenced this pull request Nov 7, 2022
rv-jenkins added a commit that referenced this pull request Nov 10, 2022
* llvm-backend/src/main/native/llvm-backend: 2c38e83 - Fix for priorities not being checked for map choices (#587)

* Sync flake inputs to submodules

* Sync flake inputs to submodules

* llvm-backend/src/main/native/llvm-backend: 611eec6 - Fix line in readme (#590)

* Sync flake inputs to submodules

Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: Radu Mereuta <[email protected]>
Baltoli pushed a commit that referenced this pull request Apr 9, 2024
With runtimeverification/haskell-backend#3637,
kore-rpc returns a new response with a `vacuous` stop reason and the
current state before rewriting the state to `#Bottom`.

Changes in this PR:
- added a new set `vacuous` to the kcfg. The reason to add the set here
and not in the `APRProof` is that the response comes from the backend,
and is not semantics related.
- modified `cterm_execute` to return if the result is vacuous.
- modified `extend` to add a `vacuous` node to the kcfg if
`cterm_execute` gets a `vacuous` response.
- modified `APRProof` and `APRBMCProof` to prevent marking `vacuous`
nodes as `pending` or `failing`.
- modified proof summaries to include `vacuous`.

<img width="827" alt="Screenshot 2023-08-08 at 16 42 48"
src="https://github.com/runtimeverification/pyk/assets/16517508/5e20228e-03e0-412f-8fb1-c5f9ac340ad9">

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
Baltoli pushed a commit that referenced this pull request Apr 9, 2024
With runtimeverification/haskell-backend#3637,
kore-rpc returns a new response with a `vacuous` stop reason and the
current state before rewriting the state to `#Bottom`.

Changes in this PR:
- added a new set `vacuous` to the kcfg. The reason to add the set here
and not in the `APRProof` is that the response comes from the backend,
and is not semantics related.
- modified `cterm_execute` to return if the result is vacuous.
- modified `extend` to add a `vacuous` node to the kcfg if
`cterm_execute` gets a `vacuous` response.
- modified `APRProof` and `APRBMCProof` to prevent marking `vacuous`
nodes as `pending` or `failing`.
- modified proof summaries to include `vacuous`.

<img width="827" alt="Screenshot 2023-08-08 at 16 42 48"
src="https://github.com/runtimeverification/pyk/assets/16517508/5e20228e-03e0-412f-8fb1-c5f9ac340ad9">

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants